Title :
Cache coherence protocol verification of a multiprocessor system with shared memory
Author :
Azizi, Mostafa ; Ait Mohamed, Otmane ; Song, Xiaoyu
Author_Institution :
LASSO-DIRO, Montreal Univ., Que., Canada
fDate :
6/20/1905 12:00:00 AM
Abstract :
In this paper, we present the verification of a multiprocessor system with shared memory, using VIS tool. This system consists of three processors; each one has its cache and all share the main memory and the bus. Its RTL-level design is described in Verilog-HDL and the properties to be verified, in CTL. Also, we establish the effect of data width upon the reachability analysis. As results, safety and liveness properties are fulfilled by the system design, and a fast increase of reachable state number and BDD (Binary Decision Diagram) size is observed when the data width or the processor number are growing. By using MDG tool, we plan to resolve the negative effect of cache size increase
Keywords :
binary decision diagrams; cache storage; formal verification; memory protocols; reachability analysis; shared memory systems; CTL; MDG tool; RTL-level design; VIS tool; Verilog-HDL; binary decision diagram; cache coherence protocol verification; multiprocessor system; reachability analysis; shared memory; Binary decision diagrams; Boolean functions; Coherence; Data structures; Formal verification; Hardware design languages; Multiprocessing systems; Protocols; Reachability analysis; Safety;
Conference_Titel :
Microelectronics, 1998. ICM '98. Proceedings of the Tenth International Conference on
Conference_Location :
Monastir
Print_ISBN :
0-7803-4969-5
DOI :
10.1109/ICM.1998.825578
