Integrating formal verification with Murφ if distributed cache coherence protocols in FAME multiprocessor system design

Flexible Architecture for Multiple Environments (FAME) is Bull architecture for large symmetrical multiprocessors based on Intel's Itanium(R) 2 family, which is used in Bull NovaScale(R) servers series. A key point in the development of this distributed shared memory architecture is the definition of its cache coherence protocol. This paper reports experiences and results of integrating formal verification of FAME cache coherence protocol, on 4 successive versions of this architecture. The goal is to find protocol definition bugs (not implementation) in the early phases of the design, focusing on: cache coherency, data integrity and deadlock-freeness properties. We have performed modeling and verification using Murphi tool and language, because of its easiness of use and its efficient state reduction techniques. The analysis of the results shows that this approach is cost-effective, and in spite of the state explosion problem, it has helped us in finding hard-to-simulate protocol bugs, before the implementation is far ahead.