An Optimized Symbolic Bounded Model Checking Engine

  • Rachel Tzoref
  • Mark Matusevich
  • Eli Berger
  • Ilan Beer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2860)


It has been shown that bounded model checking using a SAT solver can solve many verification problems that would cause BDD based symbolic model checking engines to explode. However, no single algorithmic solution has proven to be totally superior in resolving all types of model checking problems. We present an optimized bounded model checker based on BDDs and describe the advantages and drawbacks of this model checker as compared to BDD-based symbolic model checking and SAT-based model checking. We show that, in some cases, this engine solves verification problems that could not be solved by other methods.


  1. 1.
  2. 2.
    Beer, I., Ben-David, S., Eisner, C., Landver, A.: RuleBase: An industry-oriented formal verification tool. In: Design Automation Conference, June 1996, pp. 655–660 (1996)Google Scholar
  3. 3.
    Beer, I., Ben-David, S., Eisner, C., Geist, D., Gluhovsky, L., Heyman, T., Landver, A., Paanah, P., Rodeh, Y., Ronin, G., Wolfsthal, Y.: Rulebase: Model checking at IBM. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 480–483. Springer, Heidelberg (1997)Google Scholar
  4. 4.
    Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 184–194. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  5. 5.
    Bentley, B.: Validating the intel pentium 4 microprocessor. In: Design Automation Conference, pp. 244–248 (2001)Google Scholar
  6. 6.
    Bertacco, V., Olukotun, K.: Efficient state representation for symbolic simulation. In: 39th ACM/IEEE Design Automation Conference (2002)Google Scholar
  7. 7.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  8. 8.
    Bryant, R., Beatty, D., Brace, K., Cho, K., Sheffler, T.: Cosmos: A compiled simulator for mos circuits. In: Proceedings of the Design Automation Conference, pp. 9–16 (1987)Google Scholar
  9. 9.
    Bryant, R.E.: Amethodology for hardware verification based on logic simulation. Journal of the ACM (JACM) 38(2), 299–328 (1991)MATHCrossRefGoogle Scholar
  10. 10.
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Press, Norwell (1993)MATHGoogle Scholar
  11. 11.
    Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001 (2001)Google Scholar
  12. 12.
    Sheeran, M., Singh, S., Stalmarck, G.: Checking safety properties using induction and a sat-solver. In: Formal Methods in Computer Aided Design (2000)Google Scholar
  13. 13.
    Silva, G.P.M., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. on Computers, 506–516 (1999)Google Scholar
  14. 14.
    Tzoref, R., Matusevich, M., Berger, E., Beer, I.: An optimized symbolic bounded model checking engine. Technical Report H-0185, IBM Haifa Research Laboratory (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Rachel Tzoref
    • 1
  • Mark Matusevich
    • 1
  • Eli Berger
    • 1
  • Ilan Beer
    • 1
  1. 1.IBM Haifa Research LabHaifaIsrael

Personalised recommendations