Top-level Re nement in Processor Veri cationSava

We provide a framework for the speciication and veriica-tion of high-performance processors. As an example, we give a high-level speciication and correctness proof for a processor that uses speculation, register renaming, superscalar out-of-order execution, and resolution of memory dependencies. The speciications of its three concurrently operating units are very general and can be reened 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.