专利详情

专利名称	基于可满足性的组合电路等价性检验方法
申请号	CN200410007711.8	专利类型	发明专利
公开（公告）号	CN1560769	公开（授权）日	2005.01.05
申请（专利权）人	中国科学院计算技术研究所	发明（设计）人	李光辉;李晓维
主分类号	G06F17/50	IPC主分类号	G06F17/50
专利有效期	基于可满足性的组合电路等价性检验方法至基于可满足性的组合电路等价性检验方法	法律状态	授权
说明书摘要	本发明涉及超大规模集成电路设计验证技术领域，特别是组合电路的形式验证方法——等价性检验方法。该方法是以可满足性算法为引擎，增量地验证整个电路设计，所述方法具有两个阶段，第一阶段是确定两个电路内部的候选等价信号，并通过电路结构分析，对候选等价信号作静态筛选，第二阶段是通过子句分组实现增量可满足性方法，并验证每对候选信号的等价性。其主要特点在于：1)通过电路结构分析对电路内部的候选等价信号进行筛选，在验证过程中则动态地选择分割集中的等价信号，保证分割集中信号是相互独立的。2) 通过对子句进行分组，来实现增量的可满足性算法，节省计算资源，提高算法性能和处理能力。