Trace table based approach for pipelined microprocessor verification

  • Jun Sawada
  • Warren A. HuntJr.
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


This paper presents several techniques for formally verifying pipelined microprocessor implementations that contain out-of-order execution and dynamic resolution of data-dependent hazards. Our principal technique models the trace of executed instructions using a table-based representation called a MAETT. We express invariant properties of pipelined implementations by specifying relations between fields in the MAETT. To show the viability of this technique, we have proved the correctness of a simple out-of-order completion pipelined microprocessor design using the ACL2 theorem prover. This verification was performed incrementally by proving that the specified relations hold for all microarchitectural states reachable from a flushed implementation state, eventually permitting us to prove that the entire pipelined machine design implements its ISA specification.


Register File Correctness Criterion Execution Unit Architectural State Verification Approach 
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.


  1. 1.
    M. Agaard, M. Leeser, Reasoning About Pipelines with Structural Hazards, Pipelined Microprocessors, Theorem Provers in Circuit Design: theory, practice, and experience, Lecture Notes in Computer Science 901, Springer Verlag, 1995, page 13–32.Google Scholar
  2. 2.
    R. S. Boyer and J S. Moore. A Computational Logic Handbook. Academic Press, Boston, 1988.Google Scholar
  3. 3.
    J. R. Burch, D. L. Dill: Automatic Verification of Pipelined Microprocessor Control, In D. Dill Editor, Computer Aided Verification, Lecture Notes in Computer Science 818, Springer Verlag, 1994, page 68–80.Google Scholar
  4. 4.
    J. R. Burch. Techniques for verifying superscalar microprocessors. In Design Automation Conference, June 1996.Google Scholar
  5. 5.
    D. Cyrluk. Microprocessor verification in PVS: A methodology and simple example, Technical Report SRI-CSL-93-12, SRI Computer Science Laboratory, Dec. 1993Google Scholar
  6. 6.
    J. Hennessey, D. Patterson, Computer Architecture a Quantitative Approach, Morgan Kaufmann Publishers, Inc., 1996.Google Scholar
  7. 7.
    W. A. Hunt, Jr., B. Brock, A Formal HDL and Its Use in the FM9001 Verification. In C.A.R. Hoare and M.J.C. Gordon, editors, Mechanized Reasoning and Hardware Design, page 35–48. Prentice-Hall International Series in Computer Science, Engle wood Cliffs, N.J., 1992Google Scholar
  8. 8.
    R. B. Jones, D. L. Dill, J. R. Burch, Efficient Validity Checking for Processor Verification, 1995 IEEE/ACM International Conference on Computer-Aided Design, pages 2–6.Google Scholar
  9. 9.
    M. Kaufmann, J S. Moore, ACL2: An Industrial Strength Version of Nqthm, Proceedings of the Eleventh Annual Conference on Computer Assurance (COMPASS-96), pages 23–34, IEEE Computer Society Press, June 1996.Google Scholar
  10. 10.
    M. Srivas, M. Bickford, Formal Verification of a Pipelined Microprocessor, IEEE Software, September 1990, page 52–64.Google Scholar
  11. 11.
    M. K. Srivas, S. P. Miller, Formal Verification of a Commercial Microprocessor, Technical Report SRI-CSL-95-12, SRI Computer Science Laboratory, July 1995.Google Scholar
  12. 12.
    S. Tahar, R. Kumar, Formal Verification of Pipeline Conflicts in RISC Processors, Proc. European Design Automation Conference (EURO-DAC94), Grenoble, France, September 1994, IEEE Computer Society Press. page 285–289.Google Scholar
  13. 13.
    P. J. Windley, M. L. Coe, A Correctness Model for Pipelined Microprocessors, Theorem Provers in Circuit Design: theory, practice, and experience, Lecture Notes in Computer Science 901, Springer Verlag, 1995, page 33–51.Google Scholar
  14. 14.
    P. J. Windley, J. R. Burch: Mechanically Checking a Lemma Used in an Automatic Verification Tool, Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science 1166, Springer Verlag, 1996, page 362–376.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Jun Sawada
    • 1
  • Warren A. HuntJr.
    • 2
  1. 1.Department of Computer SciencesUniversity of TexasAustinUSA
  2. 2.Computational Logic, Inc.AustinUSA

Personalised recommendations