Abstract: In order to improve verification efficiency of equivalence checking in digital circuits, an approach is proposed on the combination of logic cone partition and SAT. The specification and implementation circuits are divided into several logic cones in accordance with partition rules. Logic cones of two circuits are matched using matching techniques. An “exclusive-or” gate is connected to outputs of the two matched logic cones, then the miter circuit is constructed, and the structure is changed to the corresponding conjunctive normal formula. The Miter circuit is proven to be functionally equivalent or not using the engine of satisfiability. Experimental results show the feasibility of the approach on the ISCAS’85 benchmark circuits.

Key words: equivalence checking, logic cone, satisfiability

摘要： 为了提高等价性验证在数字电路中的验证效率，提出一种逻辑锥分割和可满足性相结合的方法。通过划分规则把参照电路和实现电路划分成若干个逻辑锥，利用匹配技术对两者的逻辑锥进行匹配，将已匹配的两个逻辑锥的输出用一个异或门连接，从而得到Miter电路，将该结构转换成相应的合取范式，用可满足性引擎来验证Miter电路是否功能等价。在ISCAS’85基准电路的实验结果表明该方法的可行性。

关键词: 等价性验证, 逻辑锥, 可满足性