Addressing Hard Problems of Cache Coherence Protocols Verification Through Enhanced Directed Model Checking

Cache coherence protocols are essential in multi-core industrial processor systems. However, their increasing complexity, particularly due to the numerous rules involved in each protocol transaction, results in an exponentially expanding state space. Traditional model checking techniques, such as Murphi, demonstrate limitations in addressing this complexity. For instance, TileLink Cached (TL-C) coherence protocols, widely implemented in RISC-V open-source processors, exemplify these verification difficulties. To tackle the deep target states arising from complex protocol transactions, we design a new directed model checking framework combined with random walk. Additionally, we introduce a novel scoring function to efficiently guide the search process by leveraging variable dependencies within cache protocols. The experimental results demonstrate the effectiveness of our search framework and scoring function.