SMV Case Studies

• Ranjit Jhala and Kenneth L. McMillan, "Microarchitecture Verification by Compositional Model Checking", in G. Berry, H. Comon and A. Finkel (Eds.), Computer Aided Verification 13th International Conference, CAV 2001, LNCS 2102, Paris, France, pp. 396-410, July 18-22, 2001, Springer.

  Compositional model checking is used to verify a processor microarchitecture containing most of the features of a modern microprocessor, including branch prediction, speculative execution, out-of-order execution and a load-store buffer supporting re-ordering and load forwarding. We observe that the proof methodology scales well, in that the incremental proof cost of each feature is low. The proof is also quite concise with respect to proofs of similar microarchitecture models using other methods.

  • Paper (PS).
  • SMV source file.
• Kenneth L. McMillan, "Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking", CHARME 2001, to appear.

  We consider the formal verification of the cache coherence protocol of the Stanford FLASH multiprocessor for N processors. The proof uses the SMV proof assistant, a proof system based on symbolic model checking. The proof process is described step by step. The protocol model is derived from an earlier proof of the FLASH protocol, using the PVS system, allowing a direct comparison between the two methods.

  • Paper (PS).
  • SMV source file.