Verification of the Futurebus+ cache coherence protocol: a case study in model checking
Kylie A. Williams, Robert Esser · 2004
This paper presents a case study for automatic verifi-cation using the Communicating Sequential Processes formalism. The case study concerns the Futurebus+ cache coherency standard; we develop a formal model of the protocol and perform some verification tasks upon it. In the process of doing so, we extend the previous solution by developing a formal specification of cache coherence that is suitable for the verification of both directory and snooping based cache coherence protocols. 1