Abstract
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 it to verify the cache coherence protocol of the Cray X1. Using this approach we uncovered three architectural protocol errors and exposed several implementation errors by replaying the witness strings on the Verilog implementation.
Original language | English (US) |
---|---|
Title of host publication | Proceedings - International Parallel and Distributed Processing Symposium, IPDPS 2003 |
Publisher | Institute of Electrical and Electronics Engineers Inc. |
ISBN (Electronic) | 0769519261, 9780769519265 |
DOIs | |
State | Published - 2003 |
Event | International Parallel and Distributed Processing Symposium, IPDPS 2003 - Nice, France Duration: Apr 22 2003 → Apr 26 2003 |
Publication series
Name | Proceedings - International Parallel and Distributed Processing Symposium, IPDPS 2003 |
---|
Other
Other | International Parallel and Distributed Processing Symposium, IPDPS 2003 |
---|---|
Country/Territory | France |
City | Nice |
Period | 4/22/03 → 4/26/03 |
Bibliographical note
Publisher Copyright:© 2003 IEEE.