An ACL2 Proof of Write Invalidate Cache Coherence

As a pedagogical exercise in ACL2, we formalize and prove the correctness of a write invalidate cache scheme. In our formalization, an arbitrary number of processors, each with its own local cache, interact with a global memory via a bus which is snooped by the caches. 1 Ongoing Industrial Applications of ACL2 The ACL2 theorem proving system is nding use in industrial-scale veri cation projects. Two signi cant projects which have been reported previously are { the mechanical veri cation of the oating-point division microcode for the AMD-K5TM 6], and { the ACL2 modeling of the Motorola CAP digital signal processor and its use to prove that a pipeline hazard detection predicate was correct and that several DSP microcode applications were correct 1]. ract of a recent talk given by David Russino of Advanced Micro Devices, Inc., summarizes the current AMD work with ACL2: Formal design veri cation at AMD has focused on the elementary arithmetic oating point operations, beginning with the FDI...

• Type: Conference
• Year: 1998
• Where: CAV
• Authors: J. Strother Moore
• Keywords: ACL2, ACL2 Modeling, CAV 1998, Hardware, Veri Cation