Results of the Verification of a Complex Pipelined Machine Model
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.
KeywordsCorrectness Criterion FIFO Queue Speculative Execution Branch Prediction Branch Instruction
- 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
- 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
- Saw.Jun Sawada. Verification scripts for FM9801 pipelined microprocessor design. Web page http://www.cs.utexas.edu/users/sawada/FM9801/.
- 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: firstname.lastname@example.org.Google Scholar