Utilizing don't care states in SAT-based bounded sequential problems

ABSTRACT

Boolean Satisfiability (SAT) solvers are popular engines used throughout the verification world. Bounded sequential problems such as bounded model checking and bounded sequential equivalence checking rely on fast and robust SAT solvers. In this work, we introduce a technique that improves the performance of the underlying SAT solver for bounded sequential problems by taking advantage of a design's don't care states. We develop cost effective methods of filtering, replicating and applying the don't care states to the original problem thus reducing the search space. Experiments demonstrate the effectiveness of the proposed method on ISCAS'89 benchmarks.

REFERENCES

• 1: A. Biere, A. Cimatti, E.M. Clarke, O. Strichman and Y. Zhu, "Bounded Model Checking", in Vol. 58 Advances in Computer, Academic Press, 2003.
• 2: Gianpiero Cabodi , Sergio Nocco , Stefano Quer, Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals, Proceedings of the conference on Design, Automation and Test in Europe, p.10898, March 03-07, 2003
• 3: 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]
• 4: Srinivas Devadas , Abhijit Ghosh , Kurt Keutzer, Logic synthesis, McGraw-Hill, Inc., New York, NY, 1994
• 5: Shankar G. Govindaraju , David L. Dill , Alan J. Hu , Mark A. Horowitz, Approximate reachability with BDDs using overlapping projections, Proceedings of the 35th annual conference on Design automation, p.451-456, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277169]
• 6: Aarti Gupta , Malay Ganai , Chao Wang , Zijiang Yang , Pranav Ashar, Learning from BDDs in SAT-based bounded model checking, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.776040]
• 7: A. Gupta, M. Ganai, C. Wang, Z. Yang, P. Ashar, "Abstraction and BDDs Complement SAT-Based BMC in DiVer", Proc. of CAV, pp. 206--209, 2003.
• 8: Gary D. Hachtel , Fabio Somenzi, Logic Synthesis and Verification Algorithms, Kluwer Academic Publishers, Norwell, MA, 2000
• 9: T. Larrabee, "Test Pattern Generation Using Boolean Satisfiability," in IEEE Trans. on CAD, vol. 11, no. 1, pp. 4--15, 1992.
• 10: 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
• 11: In-Ho Moon , Jae-Young Jang , Gary D. Hachtel , Fabio Somenzi , Jun Yuan , Carl Pixley, Approximate reachability don't cares for CTL model checking, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.351-358, November 08-12, 1998, San Jose, California, United States [doi>10.1145/288548.289053]
• 12: 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]
• 13: Kavita Ravi , Kenneth L. McMillan , Thomas R. Shiple , Fabio Somenzi, Approximation and decomposition of binary decision diagrams, Proceedings of the 35th annual conference on Design automation, p.445-450, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277168]
• 14: Sean Safarpour , Andreas Veneris , Rolf Drechsler , Joanne Lee, Managing Don't Cares in Boolean Satisfiability, Proceedings of the conference on Design, automation and test in Europe, p.10260, February 16-20, 2004
• 15: F. Somenzi, "CUDD: CU decision diagram package", Public software, Colorado University, Boulder, 1997.
• 16: 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]
• 17: J.P.M. Silva and T. Glass, "Combinational Equivalence Checking using Satisfiability and Recursive Learning", Proc. of IEEE DATE, pp. 145--149, 1999.
• 18: D. Stoffel, M. Wedler, P. Warkentin and W. Kunz, "Structural FSM Traversal", in IEEE Trans. on CAD, vol. 23, no. 5, pp. 598--619, 2004.

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING
      Subjects: Computer-aided design (CAD)

General Terms:
Algorithms, Performance, Verification

Keywords:
bounded model checking, don't care states, satisfiability, sequential equivalence checking, unreachable states