The verification of cache coherence protocols
Fong Pong, Michel Dubois · 1993
In this paper we introduce a verification technique for cache coherence protocols at the behavior level. Protocols are specified by a Finite State Machine (FSM) model. The global state space is the Cartesian product of an arbitrary number of individual cache state spaces and is symbolically expanded. A global FSM characterizing the protocol behavior is built and protocol verification becomes equivalent to finding whether or not the global FSM may enter erroneous states. State expansion only takes a few steps, contrary to current approaches. The verification procedure is applied to the verification of five existing protocols Keywords: cache coherence protocol, formal verification, finite state machine, symbolic expansion and shared-memory multiprocessor. 2 The Verification of Cache Coherence Protocols Abstract In this paper we introduce a verification technique for cache coherence protocols at the behavior level. Protocols are specified by a Finite State Machine (FSM) model. The globa...