Alan Mishchenko
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.
- M. Abramovici, M. A. Breuer, and A. D. Friedman, Digital Systems testing and Testable Design, Computer Science Press, 1990.Google Scholar
- Berkeley Logic Synthesis and Verification Group, ABC: A system for sequential synthesis and verification, Release 51205. http://www.eecs.berkeley.edu/~alanmi/abc/Google Scholar
- P. Bjesse and A. Boralv, "DAG-aware circuit compression for formal verification", Proc. ICCAD '04, pp. 42--49. Google ScholarDigital Library
- D. Brand. "Verification of large synthesized designs." Proc. ICCAD '93, pp. 534--537. Google ScholarDigital Library
- R. Brayton and C. McMullen, "The decomposition and factorization of Boolean expressions," Proc. ISCAS '82, pp. 29--54.Google Scholar
- R. Brayton, G. Hachtel, A. Sangiovanni-Vincentelli, "Multilevel logic synthesis", Proc. IEEE, Vol. 78, Feb.1990.Google Scholar
- R. E. Bryant, "Graph-based algorithms for Boolean function manipulation," IEEE TC, Vol. C-35(8), Aug 1986, pp. 677--691. Google ScholarDigital Library
- R. E. Bryant, S. K. Lahiri, and S. A. Seshia, "Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions", Proc. CAV '02, LNCS, Vol. 2404, pp. 78--92. Google ScholarDigital Library
- S. Chatterjee, A. Mishchenko, R. Brayton, X. Wang, and T. Kam, "Reducing structural bias in technology mapping", Proc. ICCAD '05, pp. 519--526. http://www.eecs.berkeley.edu/~alanmi/publications/2005/iccad05_map.pdf Google ScholarDigital Library
- CSAT: UCSB circuit SAT solver: http://cadlab.ece.ucsb.edu/downloads/CSAT.htmGoogle Scholar
- 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.Google ScholarDigital Library
- N. Een, "Description of Cadence MiniSat", SAT-Race 2006. http://fmv.jku.at/sat-race-2006/Google Scholar
- 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/Google Scholar
- N. Een and N. Sörensson, "MiniSat: A SAT solver with conflict-clause minimization ". Proc. SAT '05.Google Scholar
- 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.pdfGoogle Scholar
- C. A. J. van Eijk. "Sequential equivalence checking based on structural similarities", IEEE TCAD, Vol. 19(7), 2000, pp. 814--819.Google ScholarDigital Library
- M. K. Ganai, P. Ashar, A. Gupta, L. Zhang, and S. Malik, "Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver", Proc. DAC '02, pp. 747--750. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- H. S. Jin, M. Awedh, and F. Somenzi, "CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking". Proc. CAV '04, pp. 519--522.Google Scholar
- A. Kuehlmann, A. Srinivasan, D. P. LaPotin, "Verity - A formal verification program for custom CMOS circuits", IBM J. of Research and Development, 1995, Vol. 39(1/2), pp 149--165. http://www.research.ibm.com/journal/rd/391/kuehlmann.pdf Google ScholarDigital Library
- 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.Google ScholarDigital Library
- A. Kuehlmann, "Dynamic transition relation simplification for bounded property checking". Proc. ICCAD '04, pp. 50--57. Google ScholarDigital Library
- F. Lu, L. Wang, K. Cheng, R. Huang. "A circuit SAT solver with signal correlation guided learning". Proc. DATE '03, pp. 892--897. Google ScholarDigital Library
- F. Lu, L.-C. Wang, K.-T. Cheng, J. Moondanos and Z. Hanna, "A signal correlation guided ATPG solver and its applications for solving difficult industrial cases", Proc. DAC '03, pp. 668--673. Google ScholarDigital Library
- F. Lu and K. T. Cheng, "Sequential equivalence checking based on K-th invariants and circuit SAT solving", Proc. HLDVT Workshop '05, pp. 45--52. Google ScholarDigital Library
- Y. Matsunaga, "An efficient equivalence checker for combinational circuits", Proc. DAC '96, pp. 629--634. Google ScholarDigital Library
- 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.pdfGoogle Scholar
- 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. Google ScholarDigital Library
- A. Mishchenko, S. Chatterjee, and R. Brayton, "DAG-aware AIG rewriting: A fresh look at combinational logic synthesis", Proc. DAC '06, pp. 532--536. http://www.eecs.berkeley.edu/~alanmi/publications/2006/dac06_rwr.pdf Google ScholarDigital Library
- 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.pdfGoogle Scholar
- 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.Google Scholar
- J. Moondanos, C.-J. H. Seger, Z. Hanna, and D. Kaiss, "CLEVER: Divide and conquer Combinational Logic Equivalence VERification with false negative elimination", Proc. CAV '01, pp. 131--143. Google ScholarDigital Library
- M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik. "Chaff: Engineering an efficient SAT solver". Proc. DAC '01, pp. 530--535. Google ScholarDigital Library
- MVSIS Group. MVSIS: Multi-Valued Logic Synthesis System. UC Berkeley. http://www.cad.eecs.berkeley.edu/mvsisGoogle Scholar
- 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.pdfGoogle Scholar
- E. Sentovich et al. "SIS: A system for sequential circuit synthesis." Technical Report, UCB/ERI, M92/41, ERL, Dept. of EECS, UC Berkeley, 1992.Google Scholar
- 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.Google Scholar
- J. P. Marques-Silva and L. G. e Silva, "Solving satisfiability in combinational circuits". IEEE Design and Test of Computers 2003, Vol. 20(4), pp. 16--21.Google Scholar
- 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.Google ScholarDigital Library
- A. Solar-Lezama, R. Rabbah, R. Bodik, K. Ebcioglu, "Programming by sketching for bit-streaming programs", ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '05), Chicago, IL, June 2005, pp 281--294. Google ScholarDigital Library
- M. N. Velev, "Efficient translation of Boolean formulas to CNF in formal verification of microprocessors", Proc. ASP-DAC '04, January 2004, pp. 310--315. Google ScholarDigital Library
- J. S. Zhang, A. Mishchenko, R. Brayton, and M. Chrzanowska-Jeske, "Symmetry detection for large boolean functions using circuit representation, simulation, and satisfiability", Proc. DAC '06, pp. 532--536. http://www.eecs.berkeley.edu/~alanmi/publications/2006/dac06_sym.pdf Google ScholarDigital Library
- CEC benchmarks used: http://www.eecs.berkeley.edu/~alanmi/cecGoogle Scholar
Index Terms
- Improvements to combinational equivalence checking
Recommendations
Efficient Equivalence Checking Technique for Some Classes of Finite-State Machines
AbstractFinite transducers, two-tape automata, and biautomata are related computational models descended from the concept of finite-state automaton. In these models an automaton controls two heads that read or write symbols on the tapes in the one-way ...
DP Lower bounds for equivalence-checking and model-checking of one-counter automata
We present a general method for proving DP-hardness of problems related to formal verification of one-counter automata. For this we show a reduction of the SAT-UNSAT problem to the truth problem for a fragment of (Presburger) arithmetic. The fragment ...
Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds
FoSSaCS '02: Proceedings of the 5th International Conference on Foundations of Software Science and Computation StructuresWe present a general method for proving DP-hardness of equivalence-checking problems on one-counter automata. For this we show a reduction of the Sat-Unsat problem to the truth problem for a fragment of (Presburger) arithmetic. The fragment contains ...
Comments