Heuristics for Complexity-Effective Verification of a Cache Coherence Protocol Implementation
Dennis Abts, Ying Chen, David J. Lilja · 2003
Verifying the correctness of a shared-memory multiprocessor cache coherence protocol, and its implementation in silicon, is an extraordinarily complex and time-consuming task. The detailed formal verification model developed for the Cray X1 cache coherence protocol, for instance, produces a search space with over 214 million reachable states. Exhaustively searching this space for errors in the protocol and its implementation is computationally prohibitive. To address this problem, we describe a novel method for extracting traces called "witness strings" from the formal verification process. These witness strings then are executed on a logic simulation of the hardware that implements the protocol. To reduce the number of states that need to be explored to discover an error in a coherence protocol using this verification environment, we introduce and compare several search heuristics. We show that the min-max-predict search heuristic consistently outperforms both breadth-first search (BFS) and depth-first search (DFS) for 12 protocol errors manually embedded in the Cray X1 and Stanford DASH coherence protocols. In many cases, this heuristic was able to reduce the number of states that needed to be searched by a factor of 50-100.