|
|
|---|
|
|
|
|---|
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), Springer-Verlag LNCS 1427, Heidelberg, pp. 135-146, 1998.
Relevance: proof method for dealing with exceptions
and speculative execution
Abstract
We 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 microarchitecture. Given that certain requirements are met by this table-based model, we have mechanically verified our correctness criterion using the ACL2 theorem prover.