Modeling a Cache Coherence Protocol with the Guarded Action Language

Quentin L. Meunier, Yann Thierry-Mieg, Emmanuelle Encrenaz

We present a formal model built for verification of the hardware Tera-Scale ARchitecture (TSAR), focusing on its Distributed Hybrid Cache Coherence Protocol (DHCCP). This protocol…