Using Boolean Satisfiability for Combinational Equivalence Checking

Zheng Fei-jun; Yan Xiao-lang; Ge Hai-tong; Yang Jun

Volume 27 Issue 4

Apr. 2005

Turn off MathJax

Article Contents

Article Navigation > Journal of Electronics & Information Technology > 2005 > 27(4): 651-654

Zheng Fei-jun, Yan Xiao-lang, Ge Hai-tong, Yang Jun . Using Boolean Satisfiability for Combinational Equivalence Checking[J]. Journal of Electronics & Information Technology, 2005, 27(4): 651-654.

Citation:

Zheng Fei-jun, Yan Xiao-lang, Ge Hai-tong, Yang Jun . Using Boolean Satisfiability for Combinational Equivalence Checking[J]. Journal of Electronics & Information Technology, 2005, 27(4): 651-654.

Zheng Fei-jun, Yan Xiao-lang, Ge Hai-tong, Yang Jun . Using Boolean Satisfiability for Combinational Equivalence Checking[J]. Journal of Electronics & Information Technology, 2005, 27(4): 651-654.

Citation:

Zheng Fei-jun, Yan Xiao-lang, Ge Hai-tong, Yang Jun . Using Boolean Satisfiability for Combinational Equivalence Checking[J]. Journal of Electronics & Information Technology, 2005, 27(4): 651-654.

PDF( 944 KB)

Using Boolean Satisfiability for Combinational Equivalence Checking

Received Date: 2003-11-04
Rev Recd Date: 2004-03-02
Publish Date: 2005-04-19

Abstract

Abstract

In this paper, a new combinational equivalence checking approach using Boolean Satisfiability is proposed. The algorithm uses several methods to reduce the space of the SAT reasoning first, those methods are AND/INVERTER graph transformation, BDD propagation and implication learning, CNF-based SAT solver zChaff is used to solve the verification task. The algorithm combines the advantages of both BDD and SAT, BDDs size is limited to avoid memory explosion problem and structural reduction is applied to reduce the search space of SAT. The efficiency of the proposed approach is shown through its application on the ISCAS85 benchmark circuits.

FullText(HTML)

References(1)

References

Bryant R E. Graph-based algorithms for Boolean function manipulation[J].IEEE Trans. on Computers.1986, C-35(8):677-[2]Brand D. Verification of large synthesized designs. ICCAD, San Jose, CA, 1993:534 - 537.[3]Andreas Kuehlmann, Florian Krohm. Equivalence checking using cuts and heaps. Design Automation Conference, Anaheim, CA,1997:263 - 268.[4]Moskewicz M, Madigan C, Zhao Y, Zhang L, Malik S. Chaff:Engineering an efficient SAT solver. Design Automation Conference, Las Vegas, 2001:530 - 535.Goldberg E I, Prasad M R, Brayton R K. Using SAT for combinational equivalence checking. Design Automation and Test in Europe, UK, 2001:114 - 121.[5]Andreas Kuehlmann, Viresh Paruthi, Florian Krohm, Malay K Ganai. Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans. on CAD, 2002,C-21(12): 1377- 1394.[6]Malay K Ganai, Lintao Zhang, Pranav Ashar, Aarti Gupta, Sharad Malik. Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT. Design Automation Conference, New Orleans, 2002:747 - 750.[7]Fabio Somenzi. CUDD: CU Decision Diagram package release 2.3.1( http:∥v lsi.colorado.edu/～ fabio/2001 ).[8]Matsunaga Y. An efficient equivalence checker for combinational circuits. Design Automation Conference, Las Vegas, 1996:629 - 634.

Relative Articles

Supplements(0)

Cited By

Proportional views