Advertisement

Correctness of Pipelined Machines

  • Panagiotis Manolios
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)

Abstract

The correctness of pipelined machines is a subject that has been studied extensively. Most of the recent work has used variants of the Burch and Dill notion of correctness [4]. As new features are modeled, e.g., interrupts, new notions of correctness are developed. Given the plethora of correctness conditions, the question arises: what is a reasonable notion of correctness? We discuss the issue at length and show, by mechanical proof, that variants of the Burch and Dill notion of correctness are flawed. We propose a notion of correctness based on WEBs (Well-founded Equivalence Bisimulations) [16, 19]. Briefly, our notion of correctness implies that the ISA (Instruction Set Architecture) and MA (Micro-Architecture) machines have the same observable in_nite paths, up to stuttering. This implies that the two machines satisfy the same CTL*X properties and the same safety and liveness properties (up to stuttering).

To test the utility of the idea, we use ACL2 to verify several variants of the simple pipelined machine described by Sawada in [22], [23]. Our variants extend the basic machine by adding exceptions (to deal with overflows), interrupts, and fleshed-out 128-bit ALUs (one of which is described in a netlist language). In all cases, we prove the same final theorem. We develop a methodology with mechanical support that we used to verify Sawada’s machine. The resulting proof is substantially shorter than the original and does not require any intermediate abstractions; in fact, given the definitions and some general-purpose books (collections of theorems), the proof is automatic. A practical and noteworthy feature of WEBs is their compositionality. This allows us to prove the correctness of the more elaborate machines in manageable stages.

Keywords

Proof Obligation Program Counter Interrupt Handler Mechanical Proof Uninterpreted Function 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    B. Brock, M. Kaufmann, and J. S. Moore. ACL2 theorems about commercial microprocessors. In M. Srivas and A. Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD’96), pages 275–293. Springer-Verlag, 1996.Google Scholar
  2. [2]
    M. Browne, E. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59, 1988.Google Scholar
  3. [3]
    R. E. Bryant, S. German, and M. N. Velev. Exploiting positive equality in a logic of equality with uninterpreted functions. In N. Halbwachs and D. Peled, editors, Computer-Aided Verification-CAV’ 99, volume 1633 of LNCS, pages 470–482. Springer-Verlag, 1999.CrossRefGoogle Scholar
  4. [4]
    J. R. Burch and D. L. Dill. Automatic veri_cation of pipelined microprocessor control. In Computer-Aided Verification (CAV’ 94), volume 818 of LNCS, pages pp68-80. Springer-Verlag, 1994.Google Scholar
  5. [5]
    D. Cyrluk. Microprocessor verification in PVS: A methodology and simple example. Technical Report SRI-CSL-93-12, SRI, Dec. 1993.Google Scholar
  6. [6]
    T. A. Henzinger, S. Qadeer, and S. K. Rajamani. Assume-guarantee refinement between different time scales. In N. Halbwachs and D. Peled, editors, Computer-Aided Verification CAV’ 99, volume 1633 of LNCS, pages 208–221. Springer-Verlag, 19Google Scholar
  7. [7]
    R. Hosabettu, G. Gopalakrishnan, and M. Srivas. A proof of correctness of a processor implementing Tomasulo’s algorithm without a reorder buffer. In L. Pierre and T. Kropf, editors, Correct Hardware Design and Verification Methods, 10th IFIP WG10.5 Advanced Research Working Conference, (CHARME’ 99), volume 1703 of LNCS, pages 8–22. Springer-Verlag, 1999.Google Scholar
  8. [8]
    R. Hosabettu, M. Srivas, and G. Gopalakrishnan. Decomposing the proof of correctness of a pileplined microprocessors. In A. J. Hu and M. Vardi, editors, Computer-Aided Verification CAV’ 98, volume 1427 of LNCS. Springer-Verlag, 19Google Scholar
  9. [9]
    R. Hosabettu, M. Srivas, and G. Gopalakrishnan. Proof of correctness of a processor with reorder buffer using the completion functions approach. In N. Halbwachs and D. Peled, editors, Computer-Aided Verification CAV’ 99, volume 1633 of LNCS. Springer-Verlag, 19Google Scholar
  10. [10]
    M. Kaufmann, P. Manolios, and J. S. Moore, editors. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Press, June 2000.Google Scholar
  11. [11]
    M. Kaufmann, P. Manolios, and J. S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Press, July 2000.Google Scholar
  12. [12]
    M. Kaufmann and J. S. Moore. ACL2 homepage. See URL http://www.cs.utexas.edu/users/moore/acl2.
  13. [13]
    M. Kaufmann and J. S. Moore. Structured theory development for a mechanized logic. Journal of Automated Reasoning, 2000. To appear, See URL http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html#Foundations.
  14. [14]
    P. Manolios. Homepage of Panagiotis Manolios, 2000. See URL http://www.cs.utexas.edu/users/pete.
  15. [15]
    P. Manolios. Well-founded equivalence bisimulation. Technical report, Department of Computer Sciences, University of Texas at Austin, 2000. In preparation.Google Scholar
  16. [16]
    P. Manolios, K. Namjoshi, and R. Sumners. Linking theorem proving and model-checking with well-founded bisimulation. In N. Halbwachs and D. Peled, editors, Computer-Aided Verification CAV’ 99, volume 1633 of LNCS, pages 369–379. Springer-Verlag, 19Google Scholar
  17. [17]
    K. L. McMillan. Verification of an implementation of Tomasulo’s algorithm by compositional model checking. In A. J. Hu and M. Y. Vardi, editors, Computer Aided Verification (CAV’ 98), volume 1427 of LNCS, pages 110–121. Springer-Verlag, 1998.CrossRefGoogle Scholar
  18. [18]
    R. Milner. Communication and Concurrency. Prentice-Hall, 1990.Google Scholar
  19. [19]
    K. S. Namjoshi. A simple characterization of stuttering bisimulation. In 17th Conference on Foundations of Software Technology and Theoretical Computer Science,volume 1346 of LNCS, pages 284–296, 1997.Google Scholar
  20. [20]
    D. Park. Concurrency and automata on in_nite sequences. In Theoretical Computer Science, volume 104 of LNCS, pages 167–183. Springer-Verlag, 1981.CrossRefGoogle Scholar
  21. [21]
    A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas by small domain instantiations. In N. Halbwachs and D. Peled, editors, Computer-Aided Verification CAV’ 99, volume 1633 of LNCS, pages 455–469. Springer-Verlag, 19Google Scholar
  22. [22]
    J. Sawada. Formal Verification of an Advanced Pipelined Machine. PhD thesis, University of Texas at Austin, Dec. 1999. See URL http://www.cs.utexas.edu/users/sawada/dissertation/.
  23. [23]
    J. Sawada. Verification of a simple pipelined machine model. In M. Kaufmann, P. Manolios, and J. S. Moore, editors, Computer-Aided Reasoning: ACL2 Case Studies, pages 137–150. Kluwer Academic Press, 2000.Google Scholar
  24. [24]
    J. Sawada and W. A. Hunt, Jr. Trace table based approach for pipelined micro-processor verification. In Computer Aided Verification (CAV’ 97), volume 1254 of LNCS, pages 364–375. Springer-Verlag, 1997.Google Scholar
  25. [25]
    J. Sawada and W. A. Hunt, Jr. Processor verification with precise exceptions and speculative execution. In A. J. Hu and M. Y. Vardi, editors, Computer Aided Verification (CAV’ 98), volume 1427 of LNCS, pages 135–146. Springer-Verlag, 1998.CrossRefGoogle Scholar
  26. [26]
    M. Srivas and M. Bickford. Formal verification of a pipelined microprocessor. IEEE Software, pages 52–64, Sept. 1990.Google Scholar
  27. [27]
    M. K. Srivas and S. P. Miller. Formal verification of an avionics microprocessor. Technical Report CSL-95-04, SRI International, 1995.Google Scholar
  28. [28]
    P. J. Windley and M. L. Coe. A correctness model for pipelined microprocessors. In Theorem Provers in Circuit Design, volume 901 of LNCS, pages 33–52. Springer-Verlag, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Panagiotis Manolios
    • 1
  1. 1.Department of Computer SciencesUniversity of Texas at AustinUSA

Personalised recommendations