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

计算机工程与应用 ›› 2013, Vol. 49 ›› Issue (2): 61-66.

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

岳园1，何安平2

1.西北民族大学数学与计算机科学学院，兰州 730030
2.兰州大学信息科学与工程学院，兰州 730000

出版日期:2013-01-15 发布日期:2013-01-16

Equivalence checking for combinational circuits using logic cone partition

YUE Yuan1, HE Anping2

1.School of Mathematics and Computer Science, Northwest University for Nationalities, Lanzhou 730030, China
2.School of Information Science and Engineering, Lanzhou University, Lanzhou 730000, China

Online:2013-01-15 Published:2013-01-16

摘要/Abstract

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

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

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

岳园1，何安平2. 使用逻辑锥分割的组合电路等价性验证[J]. 计算机工程与应用, 2013, 49(2): 61-66.

YUE Yuan1, HE Anping2. Equivalence checking for combinational circuits using logic cone partition[J]. Computer Engineering and Applications, 2013, 49(2): 61-66.

[1]	翟治年，王中鹏，叶绿，向坚，王富忠，庞海云. 可满足（≠，=）工作流的静态k弹性否决条件[J]. 计算机工程与应用, 2019, 55(23): 35-39.
[2]	常文静1，3，徐扬2，3，吴贯锋1，3. 基于演绎长度的学习子句删除策略[J]. 计算机工程与应用, 2018, 54(16): 30-36.
[3]	尚玉玲，彭彩军. 基于SAT的串扰时延故障测试[J]. 计算机工程与应用, 2016, 52(15): 38-42.
[4]	毕忠勤¹,陈光喜²,单美静¹. 可满足性问题全部解的求解算法[J]. 计算机工程与应用, 2009, 45(3): 35-37.
[5]	周精华,翟正军. 蚁群优化在组合电路测试生成中的应用[J]. 计算机工程与应用, 2009, 45(2): 85-87.
[6]	陈丽¹,张必英². 基于分组的启发式SAT新算法——DC&DS算法[J]. 计算机工程与应用, 2008, 44(30): 64-67.