Top-level Refinement in Processor Verification

We provide a framework for the specification and verificationof high-performance processors. As an example, we give a high-levelspecification and correctness proof for a processor that uses speculation,register renaming, superscalar out-of-order execution, and resolution ofmemory dependencies. The specifications of its three concurrently operatingunits are very general and can be refined independently, so thatour proof covers a whole family of microarchitectures. Abstract treatmentof...