Abstract
We consider the problem of bounded model checking of systems expressed in a decidable fragment of first-order logic. While model checking is not guaranteed to terminate for an arbitrary system, it converges for many practical examples, including pipelined processors. We give a new formal definition of convergence that generalizes previously stated criteria. We also give a sound semi-decision procedure to check this criterion based on a translation to quantified separation logic. Preliminary results on simple pipeline processor models are presented.
This research was supported in part by the Semiconductor Research Corporation, Contract RID 1029 and by ARO grant DAAD 19-01-1-0485.
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
Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland, Amsterdam (1954)
Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1997)
Bryant, R.E., German, S., Velev, M.N.: Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Transactions on Computational Logic 2(1), 1–41 (2001)
Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78–92. Springer, Heidelberg (2002)
Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Convergence testing in term-level bounded model checking. Technical Report CMU-CS-03-156, Carnegie Mellon University (2003)
Bultan, T., Gerber, R., Pugh, W.: Symbolic model checking of infinite state systems using Presburger arithmetic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Sequential circuit verification using symbolic model checking. In: Design Automation Conference (1991)
Burch, J.R., Dill, D.L.: Automated verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Corella, F., Zhou, Z., Song, X., Langevin, M., Cerny, E.: Multiway decision graphs for automated hardware verification. Formal Methods in System Design 10(1), 7–46 (1997)
Cyrluk, D., Narendran, P.: Ground temporal logic: a logic for hardware verification. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 247–259. Springer, Heidelberg (1994)
Graf, S., Saidi, H.: Construction of abstract state graphs using PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)
Hojati, R., Isles, A., Kirkpatrick, D., Brayton, R.K.: Verification using finite instantiations and uninterpreted functions. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 218–232. Springer, Heidelberg (1996)
Isles, A.J., Hojati, R., Brayton, R.K.: Computing reachable control states of systems modeled with uninterpreted functions and infinite memory. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 256–267. Springer, Heidelberg (1998)
Lahiri, S.K., Bryant, R.E.: Deductive verification of advanced out-of-order microprocessors. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 341–354. Springer, Heidelberg (2003)
Seshia, S.A., Bryant, R.E.: Unbounded, fully symbolic model checking of timed automata using Boolean methods. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 154–166. Springer, Heidelberg (2003)
Velev, M.N., Bryant, R.E.: Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. In: 38th Design Automation Conference, DAC 2001 (June 2001)
Zhang, L., Malik, S.: Towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 200–215. Springer, Heidelberg (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
Bryant, R.E., Lahiri, S.K., Seshia, S.A. (2003). Convergence Testing in Term-Level Bounded Model Checking. 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_31
Download citation
DOI: https://doi.org/10.1007/978-3-540-39724-3_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20363-6
Online ISBN: 978-3-540-39724-3
eBook Packages: Springer Book Archive