Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

A Comparison of Two Verification Methods for Speculative Instruction Execution

  • Conference paper
  • First Online:

Part of the book series:Lecture Notes in Computer Science ((LNCS,volume 1785))

  • 862Accesses

Abstract

In this paper we describe and compare two methodologies for verifying the correctness of a speculative out-of-order execution system with interrupts. Both methods are deductive (we use PVS) and are based on refinement. The first proof is by direct refinement to a sequential system; the second proof combines refinement with induction over the number of retirement buffer slots.

Research supported in part by a grant from the German-Israel bi-national GIF foundation and a gift from Intel.

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

  1. M. Abadi and L. Lamport. The existence of refinement mappings.Theoretical Computer Science 82(2):253–284, May 1991. 498

    Article MATH MathSciNet  Google Scholar 

  2. T. Arons and A. Pnueli. Verifying Tomasulo’s algorithm by refinement.Proceedings of the 12’th VLSI design conference, 1999. 487

    Google Scholar 

  3. S. Berezin, A. Biere, E. Clarke and Y. Zhu. Combining symbolic model checking with uninterpreted functions for out-or-order processor verification.FMCAD’98:369–386, Palo Alto, 1998. 488

    Google Scholar 

  4. W. Damm and A. Pnueli. Verifying out-of-order executions.CHARME’97:23–47, Montreal, 1997. Chapmann & Hall. 487, 490

    Google Scholar 

  5. Gwennap L. Intel’s p6 uses decoupled superscalar design.Microprocessor Report, 9(2):9–15, 1995. 487, 490

    Google Scholar 

  6. J.L. Hennessy and D.A. Patterson.Computer Architecture: A Quantitative Approach. Morgan Kaufmann Publishers Inc., 1996. 487, 490

    Google Scholar 

  7. R. Hosabett, G. Gopalakrishnan and M. Srivas. A proof of correctness of a processor implementing Tomasulo’s algorithm without a reorder buffer.CHARME’ 99. 488

    Google Scholar 

  8. K.L. McMillan. Verification of an implementation of Tomasulo’s algorithm by compositional model checking.CAV’98:110–121, 1998. 488

    Google Scholar 

  9. S. Owre, J.M. Rushby, N. Shankar, and M.K. Srivas. A tutorial on using PVS for hardware verification.Proceedings of the Second Conference on Theorem Provers in Circuit Design:167–188. FZI Publication, Universität Karlsruhe, 1994. 487

    Google Scholar 

  10. A. Pnueli, T. Arons. Verification of Data-Insensitive Circuits: An In-Order-Retirement Case Study.FMCAD’98:351–368, Palo Alto, 1998. 487

    Google Scholar 

  11. J. Sawada and Jr. W.A. Hunt. Processor verification with precise exceptions and speculative execution flushing.CAV’98:135–146, Vancouver, 1998. 488

    Google Scholar 

  12. J.U. Skakkebaek, R.B. Jones, and D.L. Dill. Formal verification of out-of-order execution using incremental flushing.CAV’98:pp 98–110, Vancouver, 1998. 488

    Google Scholar 

  13. R.M. Tomasulo. An efficient algorithm for exploiting multiple arithmetic units.IBM J. of Research and Development, 11(1):25–33, 1967. 487

    Article MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The John von Neumann Minerva Center for Verification of Reactive Systems, Weizmann Institute of Science, Rehovot, Israel

    Tamarah Arons & Amir Pnueli

Authors
  1. Tamarah Arons

    You can also search for this author inPubMed Google Scholar

  2. Amir Pnueli

    You can also search for this author inPubMed Google Scholar

Editor information

Editors and Affiliations

  1. VERIMAG, 2, Avenue de la Vignate, 38240, Gières, France

    Susanne Graf

  2. BRICS, Department of Computer Science, University of Aarhus, Ny Munkegade, 8000, Aarhus C, Denmark

    Michael Schwartzbach

Rights and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Arons, T., Pnueli, A. (2000). A Comparison of Two Verification Methods for Speculative Instruction Execution. In: Graf, S., Schwartzbach, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2000. Lecture Notes in Computer Science, vol 1785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46419-0_33

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp