@inproceedings{57119236a44e477c8def5751b6745281,
title = "So many states, so little time: Verifying memory coherence in the Cray X1",
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.",
author = "Dennis Abts and Steve Scott and Lilja, {David J.}",
year = "2003",
month = jan,
day = "1",
doi = "10.1109/IPDPS.2003.1213087",
language = "English (US)",
series = "Proceedings - International Parallel and Distributed Processing Symposium, IPDPS 2003",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
booktitle = "Proceedings - International Parallel and Distributed Processing Symposium, IPDPS 2003",
note = "International Parallel and Distributed Processing Symposium, IPDPS 2003 ; Conference date: 22-04-2003 Through 26-04-2003",
}