Verification of the Futurebus+ Cache Coherence Protocol.

摘要

We used a hardware description language to construct a formal model of the cache coherence protocol described in the draft IEEE Futurebus+ standard. By applying temporal logic m odel checking techniques, we found several errors in thee standard. Thee result of our project is a concise, comprehensible and unambiguous model of the protocol that should be useful both to the Futurebus + Working Group members, who are responsible for the protocol, and to actual designers of Futurebus + boards.