Toward Complexity-Effective Verification: A Case Study of the Cray SV2 Cache Coherence Protocol
Dennis Abts, David J. Lilja, Steve Scott · 2000
Modern large-scale multiprocessors, capable of scaling to hundreds or thousands of processors, have proven to be very difficult to design and verify in a timely manner. In particular, the verification process, i.e., proving that the design is functionally correct, is often the most time-consuming aspect of developing the system. This paper discusses the methodology and early experiences of verifying the Cray SV2 cache coherence protocol. This paper proposes a method of dealing with the verification complexity of a directory-based coherence protocol. We provide the framework for a methodology that is built on a formal model of the coherence protocol, a language, and the RTL implementation. Finally, we show how this approach was used to verify the SV2 directory-based coherence protocol at the architectural level and at the corresponding Verilog implementation level. 1 Introduction Shared-memory multiprocessors provide both scalability and a flexible programming model. These features, h...