Abstract
Bounded Model Checking (BMC) is the problem of checking if a model satisfies a temporal property in paths with bounded length k. Propositional SAT-based BMC is conducted in a gradual manner, by solving a series of SAT instances corresponding to formulations of the problem with increasing k. We show how the gradual nature can be exploited for shortening the overall verification time. The concept is to reuse constraints on the search space which are deduced while checking a k instance, for speeding up the SAT checking of the consecutive k+1 instance. This technique can be seen as a generalization of‘pervasive clauses’, a technique introduced by Silva and Sakallah in the context of Automatic Test Pattern Generation (ATPG). We define the general conditions for reusability of constraints, and define a simple procedure for evaluating them. This technique can theoretically be used in any solution that is based on solving a series of closely related SAT instances (instances with non-empty intersection between their set of clauses). We then continue by showing how a similar procedure can be used for restricting the search space of individual SAT instances corresponding to BMC invariant formulas. Experiments demonstrated that both techniques have consistent and significant positive effect.
Chapter PDF
Similar content being viewed by others
Keywords
- Satisfying Assignment
- Bounded Model Check
- Automatic Test Pattern Generation
- Constraint Sharing
- Current Partial Assignment
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS99), Lect. Notes in Comp. Sci. Springer-Verlag, 1999.
A. Biere, E. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a power pc TM microprocessor using symbolic model checking without bdds. In N. Halbwachs and D. Peled, editors, Proc. 11 th Intl. Conference on Computer Aided Verification (CAV’99), Lect. Notes in Comp. Sci. Springer-Verlag, 1999.
R. I. Brafman and H. H. Hoos. To encode or not to encode: linear planning. IJCAI, pages 988–993, 1999.
M. Davis and H. Putnam. A computing procedure for quantification theory. J. ACM, 7:201–215, 1960.
L.G.e. Silva, L.M. Silveira, and J.P.M. Silva. Algorithms for solving boolean satisfiability in combinational circuits. In Proceedings of the IEEE/ACM Design, Automation and Test in Europe Conference (DATE), March 1999.
J.F. Groote, J.W.C. Koorn, and S.F.M. van Vlijmen. The safety guaranteeing system at station Hoorn-Kersenboogerd. Logic Group Preprint Series 121, Utrecht University, 1994.
J. N. Hooker. Solving the incremental satisfiability problem. Journal of Logic Programming, 15:177–186, 1993.
J.P.M. Silva and K. A. Sakallah. Robust search algorithms for test pattern generation. In Proceedings of the IEEE Fault-Tolerant Computing Symposium, June 1997.
H. Kautz and B. Selman. Planning as satisfiability. In Proc. of the 10th European Conf. on AI, pages 359–363, 1992.
J. Kim, J. Whittemore, J.P.M. Silva, and K. A. Sakallah. Incremental boolean satisfiability and its application to delay fault testing. In IEEE/ACM International Workshop on Logic Synthesis (IWLS), June 1999.
M. Sheeran, S. Singh, and G. Stalmarck. Checking safety properties using induction and a sat-solver. In Hunt and Johnson, editors, Proc. Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD 2000), 2000.
O. Shtrichman. Tuning SAT checkers for bounded model checking. In E.A. Emerson and A.P. Sistla, editors, Proc. 12 th Intl. Conference on Computer Aided Verification (CAV’00), Lect. Notes in Comp. Sci. Springer-Verlag, 2000.
J.P.M. Silva and K. A. Sakallah. GRASP-a new search algorithm for satisfiability. Technical Report TR-CSE-292996, Univerisity of Michigen, 1996.
J.P.M. Silva and K. A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48:506–516, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shtrichman, O. (2001). Pruning Techniques for the SAT-Based Bounded Model Checking Problem. In: Margaria, T., Melham, T. (eds) Correct Hardware Design and Verification Methods. CHARME 2001. Lecture Notes in Computer Science, vol 2144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44798-9_4
Download citation
DOI: https://doi.org/10.1007/3-540-44798-9_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42541-0
Online ISBN: 978-3-540-44798-6
eBook Packages: Springer Book Archive