Abstract
Bounded Model Checking (BMC) based on Boolean Satisfiability (SAT) procedures has recently gained popularity for finding bugs in large designs. However, due to its incompleteness, there is a need to perform deeper searches for counterexamples, or a proof by induction where possible. The DiVer verification platform uses abstraction and BDDs to complement BMC in the quest for completeness. We demonstrate the effectiveness of our approach in practice on industrial designs.
Chapter PDF
Similar content being viewed by others
Keywords
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
Biere, A., Cimatti, A., Clarke, E.M., 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 manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)
McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)
Ganai, M., Zhang, L., Ashar, P., Gupta, A., Malik, S.: Combining Strengths of Circuitbased and CNF-based SAT Algorithms for a High Performance SAT Solver. In: Proceedings of Design Automation Conference (2002)
Sheeran, M., Singh, S., Stalmarck, G.: Checking Safety Properties using Induction and a SAT Solver. In: Proceedings of Formal Methods in Computer Aided Design (2000)
Baumgartner, J., Kuehlmann, A., Abraham, J.: Property Checking via Structural Analysis. In: Proceedings of Computer Aided Verification (2002)
Cabodi, G., Nocco, S., Quer, S.: SAT-based Bounded Model Checking by means of BDDbased Approximate Traversals. In: Proceedings of Design And Test Europe, DATE (2003)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Kurshan, R.P.: Computer-Aided Verification of Co-ordinating Processes: The Automata- Theoretic Approach. Princeton University Press, Princeton (1994)
Gupta, A., Ashar, P., Malik, S.: Exploiting Retiming in a Guided Simulation Based Validation Methodology. In: Proceedings of CHARME (1999)
Kuehlmann, A., Baumgartner, J.: Transformation-based Verification using Generalized Retiming. In: Proceedings of Computer Aided Verification (2001)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering a Efficient SAT Solver. In: Proceedings of Design Automation Conference (2001)
Chauhan, P., Clarke, E.M., Kukula, J., Sapra, S., Veith, H., Wang, D.: Automated Abstraction Refinement for Model Checking Large State Spaces using SAT based Conflict Analysis. In: Proceedings of Formal Methods in Computer Aided Design (2002)
Gupta, A., Casavant, A.E., Ashar, P., Liu, X.G., Mukaiyama, A., Wakabayashi, K.: Property- Specific Witness Graph Generation for Guided Simulation. In: Proceedings of VLSI Design Conference (2002)
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
Gupta, A., Ganai, M., Wang, C., Yang, Z., Ashar, P. (2003). Abstraction and BDDs Complement SAT-Based BMC in DiVer . In: Hunt, W.A., Somenzi, F. (eds) Computer Aided Verification. CAV 2003. Lecture Notes in Computer Science, vol 2725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45069-6_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-45069-6_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40524-5
Online ISBN: 978-3-540-45069-6
eBook Packages: Springer Book Archive