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

fYear

1998

fDate

6/20/1905 12:00:00 AM

Firstpage

99

Lastpage

102

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Microelectronics, 1998. ICM '98. Proceedings of the Tenth International Conference on

Conference_Location

Monastir

Print_ISBN

0-7803-4969-5

Type

conf

DOI

10.1109/ICM.1998.825578

Filename

825578