一种新颖的基于层划分的等价验证方法

Combinational Equivalence Checking Using Level Based Partition

提出了一种基于SAT问题的组合电路等价验证算法,该算法特别适用于验证有着一定相似部分的两个电路。其主要创新之处为:1)基于层划分的配对点生成方法;2)基于阈值控制的回溯过程。ISCAS'85的实例很好地证明了该算法的有效性。

An improved SAT-based framework for combinational equivalence checking (CEC) is presented, which is specifically targeted on building a robust checker to compare large circuits with some structural similarities. Two ideas fundamentally distinguish the technique from previous approaches. First, those candidate equivalent pairs to be checked are built by a level-based approach; and second, false negative pair will be handled by an effective strategy. Our experiments on the ISCAS benchmark circuits demonstrate that the outlined approach is very promising.