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.
Proceedings of the Twelvth International Conference on Computer-aided Verification (CAV 2001), Lecture Notes in Computer Science 2102, Springer-Verlag, 2001, pp. xxx-xxx.