| |
|
|
Processor Verification with Precise Exceptions and Speculative Execution
AbstractWe describe a framework for verifying a pipelined microprocessor whose implementation contains precise exceptions, external interrupts, and speculative execution. We present our correctness criterion which compares the state transitions of pipelined and non-pipelined machines in presence of external interrupts. To perform the verification, we created a table-based model of pipeline execution. This model records committed and in-flight instructions as performed by the micro-architecture. Given that certain requirements are met by this table-based model, we have mechanically verified our correctness criterion using the ACL2 theorem prover.
The postscript slides for the talk can be found here. |