Sciweavers

Share
IPPS
2003
IEEE

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

9 years 5 months ago
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
Dennis Abts, Steve Scott, David J. Lilja
Added 04 Jul 2010
Updated 04 Jul 2010
Type Conference
Year 2003
Where IPPS
Authors Dennis Abts, Steve Scott, David J. Lilja
Comments (0)
books