So Many States, So Little Time: Verifying Memory Coherence in the Cray X1

This paper investigates a complexity-effective technique for verifying a highly distributed directory-based cache coherence protocol. We develop a novel approach called “witness strings” that combines both formal and informal verification methods to expose design errors within the cache coherence protocol and its Verilog implementation. In this approach a formal execution trace is extracted during model checking of the architectural model and re-encoded to provide the input stimulus for a logic simulation of the corresponding Verilog implementation. This approach brings confidence to system architects that the logic implementation of the coherence protocol conforms to the architectural model. The feasibility of this approach is demonstrated by using

• Type: Conference
• Year: 2003
• Where: IPPS
• Authors: Dennis Abts, Steve Scott, David J. Lilja
• Keywords: Cache Coherence Protocol, Directory-based Cache Coherence, Distributed And Parallel Computing, IPPS 2003, Verilog Implementation