使用逻辑锥分割的组合电路等价性验证  

Equivalence checking for combinational circuits using logic cone partition

作　　者：岳园[1] 何安平[2] 

机构地区：[1]西北民族大学数学与计算机科学学院,兰州730030 [2]兰州大学信息科学与工程学院,兰州730000

出　　处：《计算机工程与应用》2013年第2期61-66,共6页Computer Engineering and Applications

基　　金：国家自然科学基金(No.11005054)

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

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]