Advertisement

A Proof of Correctness of a Processor Implementing Tomasulo’s Algorithm without a Reorder Buffer

  • Ravi Hosabettu
  • Ganesh Gopalakrishnan
  • Mandayam Srivas
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)

Abstract

The Completion Functions Approach was proposed in [9] as a systematic way to decompose the proof of correctness of pipelined microprocessors. The central idea is to construct the abstraction function using completion functions, one per unfinished instruction, each of which specifies the effect (on the observables) of completing the instruction. However, its applicability depends on the fact that the implementation “commits” the unfinished instructions in the pipeline in program order. In this paper, we extend the completion functions approach when this is not true and demonstrate it on an implementation of Tomasulo’s algorithm without a reorder buffer. The approach leads to an elegant decomposition of the proof of the correctness criterion, does not involve the construction of an explicit intermediate abstraction, makes heavy use of an automatic case-analysis strategy based on decision procedures and rewriting, and addresses both safety and liveness issues.

Keywords

Model Check Proof Obligation Reservation Station Correctness Criterion Execution Unit 
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. AP98.
    T. Arons and A. Pnueli. Verifying Tomasulo’s algorithm by refinement. Technical report, Weizmann Institute, 1998.Google Scholar
  2. BBCZ98.
    Sergey Berezin, Armin Biere, Edmund Clarke, and Yunshan Zu. Combining symbolic model checking with uninterpreted functions for out-of-order processor verification. In Ganesh Gopalakrishnan and Phillip Windley, editors, Formal Methods in Computer-Aided Design, FMCAD’ 98, volume 1522 of Lecture Notes in Computer Science, pages 369–386, Palo Alto, CA, USA, November 1998. Springer-Verlag.CrossRefGoogle Scholar
  3. BDL96.
    Clark Barrett, David Dill, and Jeremy Levitt. Validity checking for combinations of theories with equality. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design, FMCAD’ 96, volume 1166 of Lecture Notes in Computer Science, pages 187–201, Palo Alto, CA, November 1996. Springer-Verlag.CrossRefGoogle Scholar
  4. CRSS94.
    D. Cyrluk, S. Rajan, N. Shankar, and M. K. Srivas. Effective theorem proving for hardware verification. In Ramayya Kumar and Thomas Kropf, editors, Theorem Provers in Circuit Design, TPCD’ 94, volume 910 of Lecture Notes in Computer Science, pages 203–222, Bad Herrenalb, Germany, September 1994. Springer-Verlag.Google Scholar
  5. Hoa72.
    C.A.R. Hoare. Proof of correctness of data representations. In Acta Informatica, volume 1, pages 271–281, 1972.zbMATHCrossRefGoogle Scholar
  6. Hos99.
    Ravi Hosabettu. The Completion Functions Approach homepage, 1999. At address http://www.cs.utah.edu/~hosabett/cfa.html.
  7. HP90.
    John L. Hennessy and David A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, San Mateo, CA, 1990.Google Scholar
  8. HQR98.
    Thomas Henzinger, Shaz Qadeer, and Sriram Rajamani. You assume, we guarantee: Methodology and case studies. In Hu and Vardi [HV98], pages 440–451.Google Scholar
  9. HSG98.
    Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan. Decomposing the proof of correctness of pipelined microprocessors. In Hu and Vardi [HV98], pages 122–134.Google Scholar
  10. HSG99.
    Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan. Proof of correctness of a processor with reorder buffer using the completion functions approach. 1999. Accepted for publication in the Conference on Computer Aided Verification, Trento, Italy.Google Scholar
  11. HV98.
    Alan J. Hu and Moshe Y. Vardi, editors. Computer-Aided Verification, CAV’ 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, BC, Canada, June/July 1998. Springer-Verlag.Google Scholar
  12. McM98.
    Ken McMillan. Verification of an implementation of Tomasulo’s algorithm by compositional model checking. In Hu and Vardi [HV98], pages 110–121.Google Scholar
  13. ORSvH95.
    Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.CrossRefGoogle Scholar
  14. SH98.
    J. Sawada and W. A. Hunt, Jr. Processor verification with precise exceptions and speculative execution. In Hu and Vardi [HV98], pages 135–146.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Ravi Hosabettu
    • 1
  • Ganesh Gopalakrishnan
    • 1
  • Mandayam Srivas
    • 2
  1. 1.Department of Computer ScienceUniversity of UtahSalt Lake CityUSA
  2. 2.Computer Science LaboratorySRII InternationalMenlo ParkUSA

Personalised recommendations