Top-level Refinement in Processor Verification
Sava Krsti\'c, Byron Cook, John Launchbury, and
John Matthews
We provide a framework for the specification and
verification of high-performance processors. As an example,
we give a high-level specification and correctness proof
for a processor that uses speculation, register renaming,
superscalar out-of-order execution, and resolution of
memory dependencies. The specifications of its three
concurrently operating units are very general and can be
refined independently, so that our proof covers a whole
family of microarchitectures. Abstract treatment of data,
representation of on-the-fly instructions as transactions,
and a history table containing the full information of a
processor's run are the main features of the proof.
Wed Mar 10 13:40:45 PST 1999