Model Checking TileLink Cache Coherence Protocols by Murphi

TileLink is a standard interface used for on-chip communication within the RISC-V open-source processor ecosystem. It offers a scalable, low-latency, and coherent method of exchanging data between various components of a System-on-Chip (SoC) design, such as processors, accelerators, and memory controllers. Certain components within the SoC may include caches, and TileLink Cached(TL-C) coherence protocols are implemented to ensure cache coherence among these components. The TL-C protocols are hierarchical and can be configured to operate in either inclusive or non-inclusive modes. Due to the complexity and difficulty of these protocols, our investigation focuses on utilizing model checking techniques. In this paper, we present a novel approach to construct a simple and flexible cache hierarchy in the model checking tool Murphi. We verified the generic formal models that adhere to the recent TL-C specifications proposed by SiFive with inclusive or non-inclusive policies for the first time. In particular, we have examined the shapes of cache coherence trees and their generation within the aforementioned inclusion policies.