An ACL2 Proof of Write Invalidate Cache Coherence

10 years 8 months ago
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...
J. Strother Moore
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where CAV
Authors J. Strother Moore
Comments (0)