Results of the Verification of a Complex Pipelined Machine Model

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


Using a theorem prover, we have verified a microprocessor design, FM9801. We define our correctness criterion for processors with speculative execution and interrupts. Our verification approach defines an invariant on an intermediate abstraction that records the history of instructions. We verified the invariant first, and then proved the correctness criterion. We found several bugs during the verification process.


Correctness Criterion FIFO Queue Speculative Execution Branch Prediction Branch Instruction 
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. KM96.
    Matt Kaufmann and J Strother Moore. ACL2: An industrial strength version of nqthm. In Eleventh Annual Conference on Computer Assurance (COMPASS-96), pages 23–34. IEEE computer Society Press, June 1996.Google Scholar
  2. LL90.
    Leslie Lamport and Nancy Lynch. Distributed computing models and methods. In Handbook of Theoretical Computer Science, volume B, pages 1159–1199. The MIT Press, Cambridge, Ma., 1990.Google Scholar
  3. Saw.
    Jun Sawada. Verification scripts for FM9801 pipelined microprocessor design. Web page
  4. SH.
    Jun Sawada and Warren A. Hunt, Jr. Verification of FM9801: Out-of-order processor with speculative execution and exceptions that may execute self modifying code. Unpublished Report. Personal contact: Scholar
  5. SH98.
    Jun Sawada and Warren A. Hunt, Jr. Processor verification with precise exceptions and speculative execution. In Alan J. Hu and Moshe Y. Vardi, editors, computer Aided Verification (CAV’ 98), volume 1427 of LNCS, pages 135–146. Springer Verlag, 1998.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Jun Sawada
    • 1
  • Warren A. HuntJr.
    • 2
  1. 1.Department of Computer SciencesUniversity of Texas atAustinUSA
  2. 2.IBM Austin Research LaboratoryUSA

Personalised recommendations