JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE) ›› 2016, Vol. 51 ›› Issue (3): 116-121.doi: 10.6040/j.issn.1671-9352.0.2015.136

Previous Articles     Next Articles

An equivalence checking optimization algorithm for partial implementation combinational circuits

YUE Yuan, TIAN Shuang-liang, CHEN Xiu-ping   

  1. School of Mathematics and Computer Science, Northwest University for Nationalities, Lanzhou 730030, Gansu, China
  • Received:2015-03-30 Online:2016-03-20 Published:2016-04-07

Abstract: With the rapid development of information industry, the design complexity of chips is increasing. In a complex circuit, there are some modules of unknown function, which are called a partial implementation circuit. In order to ensure the correctness of product design, we use equivalence checking methods to verify partial implementation circuits. The paper presents an optimization algorithm based satisfiability. The first, divide a partial implementation circuit into some “logic cones”; the second, create circuits of Miter in according with matched logic cones and perform variable constraints to unknown function modules using symbolic simulation technology in Miter circuits; the last, verify CNFs of Miter circuits in turn using SAT engine. A series of experimental results are generated based on ISCAS'85 benchmark circuits containing a single unknown module and similar size combinational circuits containing some unknown modules. Those experimental data demonstrate that the algorithm can improve the detection rate of circuits.

Key words: partial implementation circuits, logic cone, SAT, equivalence checking, unknown module

CLC Number: 

  • TP399
[1] 韩俊刚, 杜慧敏. 数字硬件的形式化验证[M]. 北京: 北京大学出版社, 2001: 2-21. HAN Jungang, DU Huimin. Formal digital hardware verification[M]. Beijing: Peking University Press, 2001:2-21.
[2] PAUL M, JANETT M. Equivalence checking of digital circuits: fundamentals, principles, methods[M]. Boston: Kluwer Academic Publisher, 2004.
[3] 刘冠男, 鲍华. 等价性验证在Soc设计中的应用[J]. 中国集成电路, 2014, 23(4):37-41. LIU Guannan, BAO Hua. Logic equivalence checking for Soc design[J]. China Integrated Circuit, 2014, 23(4):37-41.
[4] 李智慧, 夏银水. 基于混合技术的时序电路等价性验证[J]. 宁波大学学报(理工版), 2010, 23(3):32-37. LI Zhihui, XIA Yinshui. Sequential equivalence checking based on mixed technology[J]. Journal of Ningbo University(Natural Science & Engineering Edition), 2010, 23(3):32-37.
[5] 李晓维, 吕涛, 李华伟, 等. 数字集成电路设计验证[M]. 北京: 科学出版社, 2010. LI Xiaowei, L(¨overU)Tao, LI Weihua, et al. Verification of digital integrated circuits design[M]. Beijing: Science Press, 2010.
[6] 杨军, 葛海通. 基于BDD的时序电路等价性验证[C] //第四届中国测试学术会议论文集. 北戴河: CTC, 2006:411- 416. YANG Jun, GE Haitong. Sequential equivalence checking based on BDD[C] //Proceedings of the 4th test conference of China. Beidaihe: CTC, 2006: 411- 416.
[7] 刘歆, 熊有伦. 基于布尔可满足性的逻辑电路等价性验证方法[J]. 微电子学与计算机, 2007, 24(11):166-168. LIU Xin, XIONG Youlun. Equivalence verification method for logic circuits based on boolean satisfiability[J]. Microelectronics & Computer, 2007, 24(11):166-168.
[8] 翁延玲, 葛海通, 严晓浪, 等. 基于等价性形式验证的逻辑综合引擎设计研究[J]. 电路与系统学报, 2007, 12(4):1-4. WENG Yanling, GE Haitong, YAN Xiaolang, et al. Synthesis engine based on equivalence checking[J]. Journal of Circuits and Systems, 2007, 12(4):1-4.
[9] 李光辉, 冯冬芹, 曾松伟. 基于电路拓扑结构分析的等价性验证方法[J]. 计算机辅助设计与图形学学报, 2008, 20(12):1557-1562. LI Guanghui, FENG Dongqin, ZENG Songwei. Combinational Equivalence checking based on circuit topology analysis[J]. Journal of Computer-Aided Design & Computer Graphics, 2008, 20(12):1557-1562.
[10] WOLFGANG G, NIEOLE D, ROLF D, et al. Verification of designs containing black boxes[C] // Proceedings of the 26th Euromicro Conference. Maastricht: IEEE Computer Society, 2000:100-105.
[11] CHRISTOPH S, BERND B. Checking equivalence for partial implementations[C] //Proceedings of the 38th Conference on Design Automation. Las Vegas: DAC, 2001:238-243.
[12] ANKUR J, VAMSI B, RAJARSHI M, et al. Testing, verification and diagnosis in the presence of unknowns[C] //In Proceedings of the 18th VLSI Test Symposium. Montreal: VTS, 2000:363-369.
[13] 郑飞君, 杨军, 葛海通, 等. 面向等价性验证的锁存器匹配算法[J]. 浙江大学学报(工学版), 2006, 40(8):1293-1296. ZHENG Feijun, YANG Jun, GE Haitong, etc. Latch mapping algorithm for equivalence checking[J]. Journal of Zhejiang University(Engineering Science), 2006, 40(8):1293-1296.
[14] 张立明, 曾海林, 赵剑, 等. 结合约束满足消除误判的等价性验证方法[J]. 吉林大学学报(工学版), 2011, 41(5):1374-1377. ZHANG Liming, ZENG Hailin, ZHAO Jian, et al. Using constraint satisfaction to elimininate false negative in equivalence checking[J]. Journal of jilin University(Engineering and Technology Edition), 2011, 41(5):1374-1377.
[15] LI Guanghui, SHAO Ming, LI Xiaowei. An efficient method for verifying designs with black boxes[J]. Chinese Journal of Computers, 2004, 27(6):796-802.
[1] SONG Hong-jie, GONG Xiang-nan, PAN Wen-hua, XU Chang-qing. Neighbor sum distinguishing total coloring of Halin graph [J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2016, 51(4): 65-67.
[2] SHI Hui-xian, LI Yong-ming. Quantitative approach for linear temporal logic based on DTMC [J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2015, 50(10): 32-39.
[3] YAO Jing-jing, XU Chang-qing. Neighbor sum distinguishing total coloring of graphs with maximum degree 3 or 4 [J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2015, 50(02): 9-13.
[4] YANG Jian-hui, FAN Qiang, ZHANG Jian-ping. Detailed level-by-level study of LMM dielectronic satellite lines for neon-like xenon [J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2014, 49(07): 28-33.
[5] LIN Chun-jin1, XU Guo-jing2. Finite time blowup of multi-dimensional Kaniadakis-Quarati equation#br# [J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2014, 49(06): 79-84.
[6] WU Di, LI Su-jian, LI Hai-tao. Time satisfaction based inventory and distribution strategies for  the click-and-brick enterprise [J]. J4, 2013, 48(6): 51-60.
[7] LI Yun1, SONG Han-feng 1,2,3*. The construction and asteroseismological analysis of  the model of hot subdwarf B star [J]. J4, 2013, 48(05): 43-50.
[8] WEI Na-na, LOU Hong-xiang*. Studies of the chemical constituents of leaves of Allium sativum L. [J]. J4, 2012, 47(1): 8-11.
[9] . On the distribution of Kloosterman sums over a finite field [J]. J4, 2009, 44(6): 7-9.
[10] REN Hui-xue,YANG Yan-zhao,LIN Ji-mao,QI Yin-shan,ZHANG Ye-qing . Synthesis and characterization of 5-bromo-3-sec-butyl-6-methyluracil [J]. J4, 2007, 42(7): 9-12 .
[11] WU Wei-wei,NING Xuan-xi . A MonteCarlo simulation approach for stochastic flow of emergency evacuation networks based on different forward directed augmented paths [J]. J4, 2006, 41(6): 71-75 .
Full text



No Suggested Reading articles found!