Abstract
We consider the formal verification of the cache coherence protocol of the Stanford FLASH multiprocessor for N processors. The proof uses the SMV proof assistant, a proof system based on symbolic model checking. The proof process is described step by step. The protocol model is derived from an earlier proof of the FLASH protocol, using the PVS system, allowing a direct comparison between the two methods.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
C.N. Ip and D.L. Dill. Better verification through symmetry. In D. Agnew, L. Claesen, and R. Camposano, editors, Computer Hardware Description Languages and their Applications, pages 87–100. Elsevier, 1993.
S. Das, D. L. Dill, and S. Park. Experience with predicate abstraction. In Computer Aided Verification (CAV’99), pages 160–171, 1999.
A. Eiriksson. Formal design of 1M-gate ASICs. In FMCAD’ 98, number 1522 in LNCS, pages 49–63. Springer, 1998.
C.N. Ip and D.L. Dill. Verifying systems with replicated components in murphi. In R. Alur and T. A. Henzinger, editors, Computer Aided Verification (CAV’96), volume 1102, pages 147–158. Springer Verlag, 1996.
J. Kuskin, D. Ofelt, M. Heinrich, J. Heinlein, R. Simoni, K. Gharachorloo, J. Chapin, D. Nakahira, J. Baxter, M. Horowitz, A. Gupta, M. Rosenblum, and J. L. Hennessy. The stanford FLASH multiprocessor. In Proc. of the 21th Annual Int’l Symp. on Comp. Arch. (ISCA’94), pages 302–313, 1994.
Leslie Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers, C-28(9):690–691, 1979.
K. L. McMillan. Verification of an infinite state systems by compositional model checking. In L. Pierre and T. Kropf, editors, Correct Hardware Design and Verification Methods (CHARME’99), volume 1703 of LNCS, pages 219–233, 1999.
K.L. McMillan and J. Schwalbe. Formal verification of the gigamax cache consistency protocol. In N. Suzuki, editor, Proceedings of the International Symposium on Shared Memory Multiprocessors. MIT Press, 1991.
S. Owre, J. Rushby, and N. Shankar. PVS: A prototype verification system. In E. Kapur, editor, Conf. on Automated Deduction (CADE’92), number 607 in LNCS. Springer-Verlag, 1992.
F. Pong and M. Dubois. The verification of cache coherence protocols. In Proc. of the 5th ACM Annual Symp. on Parallel Algorithms and Architectures (SPAA’93), pages 11–20, 1993.
S. Park and D.L. Dill. Verification of the FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions. In 8th ACM Symposium on Parallel Algorithms and Architectures, pages 288–296, Padua, Italy, 1996.
Hassen Saýdi and Susanne Graf. Construction of abstract state graphs with PVS. In Orna Grumberg, editor, Computer-Aided Verification, CAV’ 97, volume 1254, pages 72–83, Haifa, Israel, 1997. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McMillan, K.L. (2001). Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. In: Margaria, T., Melham, T. (eds) Correct Hardware Design and Verification Methods. CHARME 2001. Lecture Notes in Computer Science, vol 2144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44798-9_17
Download citation
DOI: https://doi.org/10.1007/3-540-44798-9_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42541-0
Online ISBN: 978-3-540-44798-6
eBook Packages: Springer Book Archive