Abstract
In this paper we propose a method for the deductive verification of out-of-order scheduling algorithms. We use tlpvs, our pvs model of linear temporal logic (ltl), to deductively verify the correctness of a model based on the Mips R10000 design. Our proofs use the predicted values method to verify a system including arithmetic and memory operations and speculation. In addition to the abstraction refinement traditionally used to verify safety properties, we also use fairness constraints to prove progress, allowing us to detect errors which may otherwise be overlooked.
Research supported in part by the John von Neumann Minerva Center for Verification of Reactive Systems, and the European Community IST project “Omega”.
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
Aziz, A., Baumgartner, J., Heyman, T., Singhal, V.: Model checking the IBM gigahertz processor. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 72–83. Springer, Heidelberg (1999)
Abadi, M., Lamport, L.: The existence of refinement mappings. Theoretical Computer Science 82(2), 253–284 (1991)
Arons, T., Pnueli, A.: Verifying Tomasulo’s algorithm by refinement. In: VLSI 1999, pp. 306–309 (1999)
Arons, T., Pnueli, A.: A comparison of two verification methods for speculative instruction execution. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 487–502. Springer, Heidelberg (2000)
Arons, T., Pnueli, A.: A methodology for deductive verification of outof- order execution systems based on predicted values. Technical Report MCS01-04, Weizmann Institute (2001)
Biere, A., Clarke, E., Riami, R., Zhu, Y.: Verifying safety properties of a PowerPC microprocessor using symbolic model checking without BDDs. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 60–71. Springer, Heidelberg (1999)
Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Clarke, E.M., German, S.M., Zhao, X.: Verifying the SRT division algorithm using theorem proving techniques. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 111–122. Springer, Heidelberg (1996)
Gwennap, L.: MIPS R10000 uses decoupled architecture. Microprocessor Report, pp. 18–24 (October 1994)
Hosabettu, R., Gopalakrishnan, G., Srivas, M.: Verifying microarchitectures that support speculation and exceptions. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 521–537. Springer, Heidelberg (2000)
Jhala, R., McMillan, K.: Microarchitecture verification by compositional model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 397–410. Springer, Heidelberg (2001)
Kesten, Y., Pnueli, A.: Control and data abstractions: The cornerstones of practical formal verification. STTT 2(1), 328–342 (2000)
Lahiri, S.K., Bryant, R.E.: Deductive verification of advanced out-oforder microprocessors. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 341–354. Springer, Heidelberg (2003)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)
Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS System Guide. Menlo Park, CA (November 2001)
Pnueli, A., Arons, T.: tlpvs: A pvs-based ltl verification system. In: Verification: Theory and Practice, pp. 598–625 (2003)
Sawada, J., Hunt, W.A.: Processor verification with precise excpetions and speculative execution flushing. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 135–146. Springer, Heidelberg (1998)
Skakkebaek, J.U., Jones, R.B., Dill, D.L.: Formal verification of out-oforder execution using incremental flushing. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 98–110. Springer, Heidelberg (1998)
Skakkebaek, J.U., Jones, R.B., Dill, D.L.: Reducing manual abstraction in formal verification of out-of-order execution. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 2–17. Springer, Heidelberg (1998)
Sedletsky, E., Pnueli, A., Ben-Ari, M.: Formal verification of the Ricart- Agrawala algorithm. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 325–335. Springer, Heidelberg (2000)
TLPVS Homepage, http://www.wisdom.weizmann.ac.il/~verify/tlpvs
Yeager, K.C.: The Mips R10000 superscalar microprocessor. IEEE Micro, 28–40 (April 1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Arons, T. (2004). Verification of an Advanced mips-Type Out-of-Order Execution Algorithm. In: Alur, R., Peled, D.A. (eds) Computer Aided Verification. CAV 2004. Lecture Notes in Computer Science, vol 3114. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27813-9_32
Download citation
DOI: https://doi.org/10.1007/978-3-540-27813-9_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22342-9
Online ISBN: 978-3-540-27813-9
eBook Packages: Springer Book Archive