Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols

Multicore architectures are considered inevitable, given that sequential processing hardware has hit various limits. Unfortunately, the memory system of multicore processors is a huge bottleneck. To combat this problem, one needs to design aggressively optimized cache coherence protocols. This introduces the design correctness problem for advanced cache coherence protocols which will be hierarchically organized for scalable designs. Experiences show that monolithic formal verification will not scale to hierarchical designs. Hence, one needs to handle the complexity of several coherence protocols running concurrently, i.e. hierarchical protocols, using compositional techniques. To solve the problem, we develop a family of compositional approaches all based on assume-guarantee reasoning to reducing the verification complexity. We show that for the three hierarchical protocols with certain realistic features that we developed for multiple chip-multiprocessors, more than a 20-fold improvement in terms of the number of states visited can be achieved. Also, to avoid false alarms wasting designer time, we have developed an error trace justification method to eliminate false alarms using heuristics that also capitalize on our assume-guarantee approaches. Our techniques need no special tool support. They can be carried out using the widely used Murphi model checker along with support tools for abstraction and error trace justification that we have built.