Microarchitecture Verification by Compositional Model Checking

R. Jhala and K. L. McMillan

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


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.

Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems