Abstract
The usefulness of Bounded Model Checking (BMC) based on propositional satisfiability (SAT) methods for bug hunting has already been proven in several recent work. In this paper, we present two industrial strength systems performing BMC for both verification and falsification. The first is Thunder, which performs BMC on top of a new satisfiability solver, SIMO. The second is Forecast, which performs BMC on top of a BDD package. SIMO is based on the Davis Logemann Loveland procedure (DLL) and features the most recent search methods. It enjoys static and dynamic branching heuristics, advanced back-jumping and learning techniques. SIMO also includes new heuristics that are specially tuned for the BMC problem domain. With Thunder we have achieved impressive capacity and productivity for BMC. Real designs, taken from Intel’s Pentium©4, with over 1000 model variables were validated using the default tool settings and without manual tuning. In Forecast, we present several alternatives for adapting BDD-based model checking for BMC. We have conducted comparison of Thunder and Forecast on a large set of real and complex designs and on almost all of them Thunder has demonstrated clear win over Forecast in two important aspects: capacity and productivity.
Chapter PDF
Similar content being viewed by others
References
P. A. Abdulla, P. Bjesse, and N. E’en. Symbolic reachability analisys based on SAT solvers. In Proc. of the 6th International Conference of Tools and Algorithms for Construction and Analisys of Systems (TACAS 2000), volume 1785 of LNCS, pages 411–425, Berlin, 2000. Springer.
R. Armoni, L. Fix, R. Gerth, B. Ginsburg, T. Kanza, S. Mador-Haim, E. Singerman, A. Tiemeyer, M.Y. Vardi. ForSpec: A Formal Temporal Specification Language, Submitted to ICCAD’01
I. Beer, S. Ben-David, C. Eisner, A. Landver. “RuleBase: An industry-oriented formal verification tool”. In Proc. Design Automation Conference 1996 (DAC’96).
I. Beer, C. Eisner, D. Geist, L. Gluhovsky, T. Heyman, A. Landver, P. Paanah, Y. Rodeh, G. Ronin, Y. Wolfsthal. “RuleBase: Model Checking at IBM”, Proceedings of CAV’97.
J.R. Burch, E.M. Clarke, and K.L. McMillan. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142–170, 1992.
Armin Biere, Edmund Clarke, Richard Raimi, and Yunshan Zhu. “Verifying Safety Properties of a PowerPC Microprocessor Using Symbolic Model Checking without BDDs”. Proc. of Computer Aided Verification, 1999 (CAV’99).
A. Biere, A Cimatti, E. M. Clarke, and Y. Zhu. “Symbolic model checking without BDDs“. TACAS’99
A. Biere, A. Cimatti, E. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proc. of the 36th Conference on Design Automation (DAC’ 99), pages 317–320. ACM Press, 1999.
R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293–318, September 1992.
R. J. Bayardo, Jr. and R. C. Schrag, “Using CSP Look-Back Techniques to Solve Real-World SAT Instances“, pages 203–208, Proc. AAAI, 1997.
M. Davis and G. Logemann and D. Loveland, “A machine program for theorem proving”, Journal of the ACM, vol. 5, 1962.
R. Dechter, “Enhancement Schemes for Constraint Processing: Backjumping, Learning, and Cutset Decomposition”, Artificial Intelligence, pages 273–312, vol. 41,n.3, 1990.
R. Fraer, G. Kamhi, B. Ziv, M. Vardi, L. Fix, “Efficient Reachability Computation Both for Verification and Falsification“, Proceedings of International Conference on Computer-Aided Design, (CAV’00).
J.W. Freeman, “Improvements to propositional satisfiability search algorithms”, PhD Thesis. University of Pennsylvania, 1995.
K.L. McMillan. Symbolic Model Checking: an Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.
D.A. Plaisted and S. Greenbaum, “A Structure-preserving Clause Form Translation”, Journal of Symbolic Computation, vol.2, pages=293–304, 1986.
Prover 4.0 Application Programming Reference Manual, Prover Technology AB, 2000. PPI-01-ARM-1.
P. Prosser, “Hybrid algorithms for the constraint satisfaction problem”, Computational Intelligence, vol. 9,n. 3, pages 268–299, 1993.
O. Shtrichman, “Tuning SAT checkers for Bounded Model-Checking” Proc. of Computer Aided Verification, 2000 (CAV’00).
M. Sheeran, S. Singh and G. Staalmarck, “Checking safety properties using induction and a SAT solver“ Proceedings of Formal Methods in Computer Aided Design 2000 (FMCAD00)
J.P. Marques Silva and Karem A. Sakallah. GRASP — a new search algorithm for satisfiability. Technical report, University of Michigan, April 1996.
M. Sheeran and G. Stalmarck. A tutorial on Stalmarck’s proof procedure for propositional logic. In Proc. of the 2nd International Conference on Formal Methods in Computer Aided Design (FMCAD’ 98), volume 1522 of LNCS, pages 82–99, Berlin, 1998. Springer.
G. Stalmarck. System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated From Boolean Formula. Swedish Patent No. 467076 (approved 1992), US Patent No. 5276897 (1994), European Patent No. 0403454 (1995), 1989.
A. Tacchella. “SAT Based decision procedures for knowledge representation and Formal Verification”. PhD Thesis. University of Genova. 2000.
P. F. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. In Proc. of the 12th International Conference on Computer Aided Verification (CAV 2000), volume 1855 of LNCS, pages 124–138, Berlin, 2000. Springer.
J. Yang, A. Tiemeyer. “Lazy Symbolic Model Checking”. DAC’00.
H. Zhang. SATO: An efficient propositional prover. In William McCune, editor, Proceedings of the 14th International Conference on Automated deduction, volume 1249 of LNAI, pages 272–275, Berlin, July 13–17 1997. Springer.
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
Copty, F. et al. (2001). Benefits of Bounded Model Checking at an Industrial Setting. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_43
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_43
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive