We consider the verification of a complete processor
microarchitecture, containing most of the important architectural
features of a modern microprocessor. These features include branch
prediction, speculative execution, out-of-order execution (with
in-order retirement and clean exceptions) and a load-store buffer
supporting re-ordering of memory operations and load forwarding. We
observe that the proof methodology scales well, in the sense that
the incremental proof cost of each architectural feature is low, and
that the interaction of these features does not make the proof
expand intractably. The resulting proof is also quite concise with
respect to proofs of similar microarchitecture models using other
methods.
