Abstract
Model checking is a formal technique for automatically verifying that a finite-state model satisfies a temporal property. In model checking, generally Binary Decision Diagrams (BDDs) are used to efficiently encode the transition relation of the finite-state model. Recently model checking algorithms based on Boolean satisfiability (SAT) procedures have been developed to complement the traditional BDD-based model checking. These algorithms can be broadly classified into three categories: (1) bounded model checking which is useful for finding failures (2) hybrid algorithms that combine SAT and BDD based methods for unbounded model checking, and (3) purely SAT-based unbounded model checking algorithms. The goal of this paper is to provide a uniform and comprehensive basis for evaluating these algorithms. The paper describes eight bounded and unbounded techniques, and analyzes the performance of these algorithms on a large and diverse set of hardware benchmarks.
Chapter PDF
Similar content being viewed by others
References
Amla, N., Kurshan, R., McMillan, K., Medel, R.: Experimental analysis of different techniques for bounded model checking. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 34–48. Springer, Heidelberg (2003)
Amla, N., McMillan, K.: A hybrid of counterexample-based and proof-based abstraction. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 260–274. Springer, Heidelberg (2004)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)
Bryant, R.E.: Graph-based algorithms for boolean function manipulations. IEEE Transactions on Computers (1986)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 1020 states and beyond. In: LICS (1990)
Chauhan, P., Clarke, E., Kukula, J., Sapra, S., Veith, H., Wang, D.: Automated abstraction refinement for model checking large state spaces using sat based conflict analysis. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517. Springer, Heidelberg (2002)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131. Springer, Heidelberg (1982)
Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 436. Springer, Heidelberg (2001)
Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, Formal Models and Sematics, vol. B (1990)
Ganai, M., Gupta, A., Ashar, P.: Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. In: ICCAD (2004)
Goldberg, E., Novikov, Y.: Berkmin: A fast and robust sat-solver. In: DATE (2002)
Iyer, M., Parthasarathy, G., Cheng, K.T.: SATORI- an efficient sequential SAT solver for circuits. In: ICCAD (2003)
Jin, H., Somenzi, F.: CirCUs: Hybrid satisfiability solver. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 211–223. Springer, Heidelberg (2005)
Kuehlmann, A.: Dynamic transition relation simplification for bounded property checking. In: ICCAD (2004)
Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.: Robust Boolean reasoning for equivalence checking and functional property verification. In: TCAD (2003)
Kupferman, O., Vardi, M.: Model checking of safety properties. Formal Methods in System Design (2001)
Kurshan, R.: Computer-aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)
Li, B., Wang, C., Somenzi, F.: A satisfiability-based approach to abstraction refinement in model checking. In: Workshop on BMC (2003)
Marques-Silva, J., Sakallah, K.: GRASP: A search algorithm for propositional satisfiability. IEEETC: IEEE Transactions on Computers 48 (1999)
McMillan, K.: Applying SAT methods in unbounded symbolic model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725. Springer, Heidelberg (2003)
McMillan, K.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)
McMillan, K., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 2–17. Springer, Heidelberg (2003)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC (2001)
Parthasarathy, G., Iyer, M., Cheng, K.T., Wang, L.C.: A comparison of BDDs, BMC, and sequential SAT for model checking. In: High-Level Design Validation and Test Workshop (2003)
Prasad, M., Biere, A., Gupta, A.: A survey of recent advances in sat-based formal verification. In: STTT (2005)
Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proc. of the 5th International Symposium on Programming (1982)
Sheeran, M., Singh, S., Stalmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)
Wang, C., Li, B., Jin, H., Hachtel, G., Somenzi, F.: Improving ariadne’s bundle by following multiple threads in abstraction refinement. In: ICCAD (2003)
Whittemore, J., Kim, J., Sakallah, K.: Satire: A new incremental satisfiability engine. In: DAC (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amla, N., Du, X., Kuehlmann, A., Kurshan, R.P., McMillan, K.L. (2005). An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment. In: Borrione, D., Paul, W. (eds) Correct Hardware Design and Verification Methods. CHARME 2005. Lecture Notes in Computer Science, vol 3725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11560548_20
Download citation
DOI: https://doi.org/10.1007/11560548_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29105-3
Online ISBN: 978-3-540-32030-2
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science