Top-level Reenement in Processor Veriication

We provide a framework for the speci cation and veri cation of high-performance processors. As an example, we give a high-level speci cation and correctness proof for a processor that uses speculation, register renaming, superscalar out-of-order execution, and resolution of memory dependencies. The speci cations of its three concurrently operating units are very general and can be re ned independently, so that our proof covers a whole family of microarchitectures. Abstract treatment of data, representation of on-they instructions as transactions, and a history table containing the full information of a processor's run are the main features of the proof.