Abstract
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.
Chapter PDF
References
CUDD-2.3.1, http://vlsi.Colorado.edu/fabio
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)
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)
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)
Bentley, B.: Validating the intel pentium 4 microprocessor. In: Design Automation Conference, pp. 244–248 (2001)
Bertacco, V., Olukotun, K.: Efficient state representation for symbolic simulation. In: 39th ACM/IEEE Design Automation Conference (2002)
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)
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)
Bryant, R.E.: Amethodology for hardware verification based on logic simulation. Journal of the ACM (JACM) 38(2), 299–328 (1991)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Press, Norwell (1993)
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)
Sheeran, M., Singh, S., Stalmarck, G.: Checking safety properties using induction and a sat-solver. In: Formal Methods in Computer Aided Design (2000)
Silva, G.P.M., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. on Computers, 506–516 (1999)
Tzoref, R., Matusevich, M., Berger, E., Beer, I.: An optimized symbolic bounded model checking engine. Technical Report H-0185, IBM Haifa Research Laboratory (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tzoref, R., Matusevich, M., Berger, E., Beer, I. (2003). An Optimized Symbolic Bounded Model Checking Engine. In: Geist, D., Tronci, E. (eds) Correct Hardware Design and Verification Methods. CHARME 2003. Lecture Notes in Computer Science, vol 2860. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39724-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-39724-3_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20363-6
Online ISBN: 978-3-540-39724-3
eBook Packages: Springer Book Archive