Improvements to combinational equivalence checking

ABSTRACT

The paper explores several ways to improve the speed and capacity of combinational equivalence checking based on Boolean satisfiability (SAT). State-of-the-art methods use simulation and BDD/SAT sweeping on the input side (i.e. proving equivalence of some internal nodes in a topological order), interleaved with attempts to run SAT on the output (i.e. proving equivalence of the output to constant 0). This paper improves on this method by (a) using more intelligent simulation, (b) using CNF-based SAT with circuit-based decision heuristics, and (c) interleaving SAT with low-effort logic synthesis. Experimental results on public and industrial benchmarks demonstrate substantial reductions in runtime, compared to the current methods. In several cases, the new solver succeeded in solving previously unsolved problems.

REFERENCES

• 1: M. Abramovici, M. A. Breuer, and A. D. Friedman, Digital Systems testing and Testable Design, Computer Science Press, 1990.
• 2: Berkeley Logic Synthesis and Verification Group, ABC: A system for sequential synthesis and verification, Release 51205. http://www.eecs.berkeley.edu/~alanmi/abc/
• 3: P. Bjesse , A. Boralv, DAG-aware circuit compression for formal verification, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.42-49, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382541]
• 4: Daniel Brand, Verification of large synthesized designs, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.534-537, November 07-11, 1993, Santa Clara, California, United States
• 5: R. Brayton and C. McMullen, "The decomposition and factorization of Boolean expressions," Proc. ISCAS '82, pp. 29--54.
• 6: R. Brayton, G. Hachtel, A. Sangiovanni-Vincentelli, "Multilevel logic synthesis", Proc. IEEE, Vol. 78, Feb.1990.
• 7: Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
• 8: Randal E. Bryant , Shuvendu K. Lahiri , Sanjit A. Seshia, Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions, Proceedings of the 14th International Conference on Computer Aided Verification, p.78-92, July 27-31, 2002
• 9: S. Chatterjee , A. Mishchenko , R. Brayton , X. Wang , T. Kam, Reducing structural bias in technology mapping, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.519-526, November 06-10, 2005, San Jose, CA
• 10: CSAT: UCSB circuit SAT solver: http://cadlab.ece.ucsb.edu/downloads/CSAT.htm
• 11: A. Darringer, W. H. Joyner, Jr., C. L. Berman, L. Trevillyan, "Logic synthesis through local transformations," IBM J. of Research and Development, Vol. 25(4), 1981, pp 272--280.
• 12: N. Een, "Description of Cadence MiniSat", SAT-Race 2006. http://fmv.jku.at/sat-race-2006/
• 13: N. Een and N. Sörensson, "An extensible SAT-solver", Proc. SAT '03, pp. 502--518. http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
• 14: N. Een and N. Sörensson, "MiniSat: A SAT solver with conflict-clause minimization ". Proc. SAT '05.
• 15: N. Een and N. Sörensson, "Translating pseudo-Boolean constraints into SAT". Vol. 2 (2006), pp. 1--26. http://jsat.ewi.tudelft.nl/content/volume2/JSAT2_1_Een.pdf
• 16: C. A. J. van Eijk. "Sequential equivalence checking based on structural similarities", IEEE TCAD, Vol. 19(7), 2000, pp. 814--819.
• 17: Malay K. Ganai , Pranav Ashar , Aarti Gupta , Lintao Zhang , Sharad Malik, Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.514105]
• 18: L. Hellerman, "A catalog of three-variable Or-Inverter and And-Inverter logical circuits", IEEE Trans. Electron. Comput., Vol. EC-12, June 1963, pp. 198--223.
• 19: H. S. Jin, M. Awedh, and F. Somenzi, "CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking". Proc. CAV '04, pp. 519--522.
• 20: A. Kuehlmann , A. Srinivasan , D. P. LaPotin, Verity—a formal verification program for custom CMOS circuits, IBM Journal of Research and Development, v.39 n.1-2, p.149-165, Jan./March 1995
• 21: A. Kuehlmann, V. Paruthi, F. Krohm, and M. K. Ganai, "Robust boolean reasoning for equivalence checking and functional property verification", IEEE Trans. CAD, Vol. 21(12), 2002, pp. 1377--1394.
• 22: A. Kuehlmann, Dynamic transition relation simplification for bounded property checking, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.50-57, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382542]
• 23: Feng Lu , Li-C. Wang , Kwang-Ting Cheng , Ric C-Y Huang, A Circuit SAT Solver With Signal Correlation Guided Learning, Proceedings of the conference on Design, Automation and Test in Europe, p.10892, March 03-07, 2003
• 24: Feng Lu , Li-C. Wang , K.-T. (Tim) Cheng , John Moondanos , Ziyad Hanna, A signal correlation guided ATPG solver and its applications for solving difficult industrial cases, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775947]
• 25: Feng Lu , K.-T. Cheng, Sequential equivalence checking based on k-th invariants and circuit SAT solving, Proceedings of the High-Level Design Validation and Test Workshop, 2005. on Tenth IEEE International, p.45-51, November 30-December 02, 2005 [doi>10.1109/HLDVT.2005.1568812]
• 26: Yusuke Matsunaga, An efficient equivalence checker for combinational circuits, Proceedings of the 33rd annual conference on Design automation, p.629-634, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240637]
• 27: A. Mishchenko, S. Chatterjee, R. Jiang, and R. K. Brayton, "FRAIGs: A unifying representation for logic synthesis and verification". ERL Technical Report, EECS Dept., UC Berkeley, March 2005. http://www.eecs.berkeley.edu/~alanmi/publications/2005/tech05_fraigs.pdf
• 28: A. Mishchenko, J. S. Zhang, S. Sinha, J. R. Burch, R. Brayton, and M. Chrzanowska-Jeske, "Using simulation and satisfiability to compute flexibilities in Boolean networks", IEEE Trans. CAD, May 2006, Vol. 25(5), pp. 743--755.
• 29: Alan Mishchenko , Satrajit Chatterjee , Robert Brayton, DAG-aware AIG rewriting a fresh look at combinational logic synthesis, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA [doi>10.1145/1146909.1147048]
• 30: A. Mishchenko, S. Chatterjee, R. Brayton, and P. Pan, "Integrating logic synthesis, technology mapping, and retiming", ERL Technical report, April 2006. http://www.eecs.berkeley.edu/~alanmi/publications/2006/tech06_int.pdf
• 31: I.-H. Moon and C. Pixley, "Non-miter-based combinational equivalence checking by comparing BDDs with different variable orders". Proc. FMCAD '04, pp. 144--158.
• 32: John Moondanos , Carl-Johan H. Seger , Ziyad Hanna , Daher Kaiss, CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination, Proceedings of the 13th International Conference on Computer Aided Verification, p.131-143, July 18-22, 2001
• 33: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 34: MVSIS Group. MVSIS: Multi-Valued Logic Synthesis System. UC Berkeley. http://www.cad.eecs.berkeley.edu/mvsis
• 35: Ya. Novikov and R. Brinkmann, "Foundations of hierarchical SAT-solving". ZIB -Report 05-38, August 2005. Konrad-Zuse-Zentrum für Informationstechnik Berlin, Germany. http://www.zib.de/Publications/Reports/ZR-05-38.pdf
• 36: E. Sentovich et al. "SIS: A system for sequential circuit synthesis." Technical Report, UCB/ERI, M92/41, ERL, Dept. of EECS, UC Berkeley, 1992.
• 37: L. G. e Silva, L. M. Silveira, and J. P. Marques-Silva, "Algorithms for solving Boolean satisfiability in combinational circuits". Proc. DATE '99, pp. 526--530.
• 38: João Marques-Silva , Luís Guerra e Silva, Solving Satisfiability in Combinational Circuits, IEEE Design & Test, v.20 n.04, p.16-21, January 2003 [doi>10.1109/MDT.2003.1214348]
• 39: G. L. Smith, R. J. Bahnsen, H. Halliwell, "Boolean comparison of hardware and flowcharts". IBM J. of Research and Development, Vol. 26(1), 1982, pp. 106--116.
• 40: Armando Solar-Lezama , Rodric Rabbah , Rastislav Bodík , Kemal Ebcioğlu, Programming by sketching for bit-streaming programs, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 41: Miroslav N. Velev, Efficient translation of boolean formulas to CNF in formal verification of microprocessors, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, January 27-30, 2004, Yokohama, Japan
• 42: Jin S. Zhang , Alan Mishchenko , Robert Brayton , Malgorzata Chrzanowska-Jeske, Symmetry detection for large Boolean functions using circuit representation, simulation, and satisfiability, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA [doi>10.1145/1146909.1147044]
• 43: CEC benchmarks used: http://www.eecs.berkeley.edu/~alanmi/cec

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.1 Design Styles
          Subjects: Combinational logic
  B.8 Performance and Reliability
      B.8.1 Reliability, Testing, and Fault-Tolerance
      B.8.2 Performance Analysis and Design Aids

General Terms:
Design, Performance, Verification