2004 | OriginalPaper | Chapter
Integrating Formal Verification with Murφ of Distributed Cache Coherence Protocols in FAME Multiprocessor System Design
Author : Ghassan Chehaibar
Published in: Formal Techniques for Networked and Distributed Systems – FORTE 2004
Publisher: Springer Berlin Heidelberg
Included in: Professional Book Archive
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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 Murφ 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.