Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

Formal verification of out-of-order execution using incremental flushing

  • Regular Papers
  • Conference paper
  • First Online:

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

Included in the following conference series:

  • 494Accesses

Abstract

We present a two-part approach for verifying out-of-order execution. First, the complexity of out-of-order issue and scheduling is handled by creating an in-order abstraction of the out-of-order execution core. Second,incremental flushing addresses the complexity difficulties encountered by automated abstraction functions on very deep pipelines. We illustrate the techniques on a model of a simple out-of-order processor core.

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. C. Barrett, D. L. Dill, and J. Levitt. Validity checking for combinations of theories with equality. InFMCAD '96, volume 1166 ofLNCS, pages 187-201, Stanford, CA, USA, November 1996. Springer-Verlag.

    Google Scholar 

  2. J. R. Burch. Techniques for verifying superscalar microprocessors. InDAC, pages 552–557, Las Vegas, Nevada, USA, June 1996. ACM Press.

    Google Scholar 

  3. J. R. Burch and D. L. Dill. Automatic verification of microprocessor control. In David L. Dill, editor, CAV, volume 818 of LNCS, pages 68-80, Stanford, California, USA, June 1994. Springer-Verlag.

    Google Scholar 

  4. W. Damm and A. Pnueli. Verifying out-of-order executions. In H.F. Li and D.K. Probst, editors,CHARME '97, pages 23–47, Montreal, Canada, October 1997. Chapman & Hall.

    Google Scholar 

  5. J. L. Hennessy and D. A. Patterson.Computer Architecture: A Quantitative Approach. Morgan Kaufmann, 1990.

    Google Scholar 

  6. T. A. Henzinger, S. Qadeer, and S. K. Rajamani. You assume, we guarantee: Methodology and case studies. Technical report, Electronics Research Lab, Univ. of Californaia, Berkeley, CA 94720, 1998.

    Google Scholar 

  7. R. B. Jones, D. L. Dill, and J. R. Burch. Efficient validity checking for processor verification. InICCAD'95, November 1995.

    Google Scholar 

  8. R. B. Jones, C.-J. H. Seger, and D. L. Dill. Self-consistency checking. InFMCAD '96, volume 1166 ofLNCS, pages 159-171, Stanford, CA, USA, November 1996. Springer-Verlag.

    Google Scholar 

  9. B. Jonsson. On decomposing and refining specifications of distributed systems. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors,Stepwise Refinement of Distributed Systems. Models, Formalisms, Correctness., volume 430 ofLNCS, pages 361–385, Mook, The Netherlands, May-June 1989. Springer-Verlag.

    Google Scholar 

  10. S. Katz. Refinement with global equivalence proofs in temporal logic. In D. A. Peled, V R. Pratt, and G. J. Holzmann, editors,Partial Order Methods in Verification, volume 29 ofDIMACS, Series in Discrete Mathematics and Theoretical Computer Science, pages 59–78, Princeton, NJ, USA, 1996. Amer. Math. Society.

    Google Scholar 

  11. K. McMillan. Verification of an implementation of Tomasulo's algorithm by compositional model checking. Appears in this volume.

    Google Scholar 

  12. S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. K. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T.A. Henzinger, editors,CAV '96, volume 1102 ofLNCS, pages 411–414, New Brunswick, NJ, July/Aug 1996. Springer-Verlag.

    Google Scholar 

  13. J. Sawada and W. A. Hunt. Processor verification with precise exceptions and speculative execution. Appears in this volume.

    Google Scholar 

  14. J. Sawada and W. A. Hunt. Trace table based approach for pipelined microprocessor verification. In Orna Grumberg, editor,CAV '97, volume 1254 ofLNCS, pages 364–375, Haifa, Israel, June 1997. Springer-Verlag.

    Google Scholar 

  15. P J. Windley and J. R. Burch. Mechanically checking a lemma used in an automatic verification tool. InFMCAD'96, pages 362–376, November 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Systems Laboratory, Stanford University, 94305, Stanford, CA, USA

    Jens U. Skakkebæk, Robert B. Jones & David L. Dill

  2. Strategic CAD Labs, Intel, JFT-104, 2111 NE 25th Ave., 97124, Hillsboro, OR, USA

    Robert B. Jones

Authors
  1. Jens U. Skakkebæk

    You can also search for this author inPubMed Google Scholar

  2. Robert B. Jones

    You can also search for this author inPubMed Google Scholar

  3. David L. Dill

    You can also search for this author inPubMed Google Scholar

Editor information

Alan J. Hu Moshe Y. Vardi

Rights and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Skakkebæk, J.U., Jones, R.B., Dill, D.L. (1998). Formal verification of out-of-order execution using incremental flushing. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028737

Download citation

Publish with us

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