A Case Study on the Verification of Cache Coherence Protocols
Mostafa Azizi, Xiaoyu Song, E.M. Aboulhamid · International Journal of Computers and Applications · 2004
AbstractThis article presents a case study on verifying formally a multiprocessor system with shared memory using the model-checking technique. The system consists of a set of processors where each processor has its own cache, the shared main memory and the bus. The RTL (Register Transfer Level) design of the system is described in a Verilog-HDL code, and the behaviour is specified by a set of CTL (Computation Tree Logic) properties. We establish the effect of data width upon the reachability analysis. We successfully verify a set of critical safety and liveness properties for the system design. The experiments demonstrate the effectiveness of our methods. The verification results manifest the relationship between the state space, BDD (Binary Decision Diagram) size, and the verification time when the data width and the number of processors increase.