Learning from BDDs in SAT-based bounded model checking

ABSTRACT

Bounded Model Checking (BMC) based on Boolean Satisfiability (SAT) procedures has recently gained popularity as an alternative to BDD-based model checking techniques for finding bugs in large designs. In this paper, we explore the use of learning from BDDs, where learned clauses generated by BDD-based analysis are added to the SAT solver, to supplement its other learning mechanisms. We propose several heuristics for guiding this process, aimed at increasing the usefulness of the learned clauses, while reducing the overheads. We demonstrate the effectiveness of our approach on several industrial designs, where BMC performance is improved and the design can be searched up to a greater depth by use of BDD-based learning.

REFERENCES

• 1: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 2: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 3: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 4: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 5: João P. Marques-Silva , Karem A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, v.48 n.5, p.506-521, May 1999 [doi>10.1109/12.769433]
• 6: Hantao Zhang, SATO: An Efficient Propositional Prover, Proceedings of the 14th International Conference on Automated Deduction, p.272-275, July 13-17, 1997
• 7: 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]
• 8: E. Goldberg , Y. Novikov, BerkMin: A Fast and Robust Sat-Solver, Proceedings of the conference on Design, automation and test in Europe, p.142, March 04-08, 2002
• 9: O. Strichman, "Pruning Techniques for the SAT-based bounded model checking," in Proceedings of Workshop on Tools and Algorithms for the Analysis and Construction of Systems (TACAS), 2001.
• 10: Gunnar Andersson , Per Bjesse , Byron Cook , Ziyad Hanna, A proof engine approach to solving combinational design automation problems, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.514101]
• 11: M. Abramovici, M. A. Breuer, and A. D. Friedman, Digital Systems Testing and Testable Design: Computer Science Press, 1990.
• 12: Jawahar Jain , Rajarshi Mukherjee , Masahiro Fujita, Advanced verification techniques based on learning, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.420-426, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217564]
• 13: W. Kunz, D. Pradhan, and S. M. Reddy, "A Novel Framework for Logic Verification in a Synthesis Environment," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 15, pp. 20--32, 1996.
• 14: Aarti Gupta , Pranav Ashar, Integrating a Boolean Satisfiability Checker and BDDs for Combinational Equivalence Checking, Proceedings of the Eleventh International Conference on VLSI Design: VLSI for Signal Processing, p.222, January 04-07, 1998
• 15: Jerry R. Burch , Vigyan Singhal, Tight integration of combinational verification methods, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.570-576, November 08-12, 1998, San Jose, California, United States [doi>10.1145/288548.289088]
• 16: Andreas Kuehlmann , Malay K. Ganai , Viresh Paruthi, Circuit-based Boolean Reasoning, Proceedings of the 38th conference on Design automation, p.232-237, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378470]
• 17: Aarti Gupta , Zijiang Yang , Pranav Ashar , Anubhav Gupta, SAT-Based Image Computation with Application in Reachability Analysis, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.354-371, November 01-03, 2000
• 18: Poul Frederick Williams , Armin Biere , Edmund M. Clarke , Anubhav Gupta, Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking, Proceedings of the 12th International Conference on Computer Aided Verification, p.124-138, July 15-19, 2000
• 19: Parosh Aziz Abdulla , Per Bjesse , Niklas Eén, Symbolic Reachability Analysis Based on SAT-Solvers, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.411-425, March 25-April 02, 2000
• 20: Andreas Kuehlmann , Florian Krohm, Equivalence checking using cuts and heaps, Proceedings of the 34th annual conference on Design automation, p.263-268, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266090]
• 21: Martin Davis , George Logemann , Donald Loveland, A machine program for theorem-proving, Communications of the ACM, v.5 n.7, p.394-397, July 1962 [doi>10.1145/368273.368557]
• 22: Slawomir Pilarski , Gracia Hu, SAT with partial clauses and back-leaps, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.514104]
• 23: F. Somenzi, "CUDD: University of Colorado Decision Diagram Package, http://vlsi.colorado.edu/~fabio/CUDD/," 1998.
• 24: 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]
• 25: R. Brayton, F. Somenzi, and others, "VIS: Verification Interacting with Synthesis, http://vlsi.colorado.edu/~vis," 2002.

INDEX TERMS

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

General Terms:
Algorithms, Experimentation, Performance

Keywords:
BDD learning, BDDs, SAT, SAT solvers, boolean satisfiability, bounded model checking, learning, property checking