Abstract
We used a hardware description language to construct a formal model of the cache coherence protocol described in the IEEE Futurebus+standard. By applying temporal logic model checking techniques, we found errors in the standard. The result of our project is a concise, comprehensible and unambiguous model of the protocol that should be useful both to the Futurebus+Working Group members, who are responsible for the protocol, and to actual designers of Futurebus+boards.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
R.E. Bryant, “Graph-based algorithms for boolean function manipulation.”IEEE Transactions on Computers, C-35(8), 1986.
J.R. Burch, E.M. Clarke, and D.E. Long, “Representing circuits more efficiently in symbolic model checking.” InProceedings of the 28th ACM/IEEE Design Automation Conference. IEEE Computer Society Press, June 1991.
J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill, “Sequential circuit verification using symbolic model checking.” InProceedings of the 27th ACM/IEEE Design Automation Conference. ACM/IEEE, IEEE Computer Society Press, June 1990.
J.R. Burch, E.M. Clarke, K.L. McMillan, D. L. Dill, and H. Hwang, “Symbolic model checking: 1020 states and beyond.” InProceedings of the Fifth Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1990.
E.M. Clarke and E.A. Emerson, “Synthesis of synchronization skeletons for branching time temporal logic.” InLogic of Programs: Workshop, Yorktown, Heights, NY, May 1981, volume 131 ofLecture Notes in Computer Science. Springer-Verlag, 1981.
E.M. Clarke, E.A. Emerson, and A.P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications.”ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
P. Dixon, “Multilevel cache architectures”. Minutes of the Futurebus+ Working Group meeting, December 1988.
IEEE Computer Soceity.IEEE Standard for Futurebus+—Logical Protocol Specification, March 1992. IEEE Standard 896.1-1991.
D.E. Long,Model Checking, Abstraction, and Compositional Verification. Ph.D. thesis, Carnegie Mellon University, 1993.
K.L. McMillan.Symbolic Model Checking: An Approach to the State Explosion Problem. Ph.D. thesis, Carnegie Mellon University, 1992.
K.L. McMillan and J. Schwalbe, “Formal verification of the Encore Gigamax cache consistency protocol”. InProceedings of the 1991 International Symposium on Shared Memory Multiprocessors, April 1991.
A. Pnueli, “A temporal logic of concurrent programs.”Theoretical Computer Science, 13:45–60, 1981.
J.P. Quielle and J. Sifakis, “Specification and verification of concurrent systems in CESAR”. InProceedings of the Fifth International Symposium in Programming, 1981.
Author information
Authors and Affiliations
Additional information
This research was sponsored in part by the Avionics Laboratory, Wright Research and Development Center, Aeronautical Systems Division (AFSC), U.S. AIR Force, Wright-Patterson AFB, Ohio 45433–6543 under contract F33615-90-C-1465, ARPA Order No. 7597 and in part by the National Science Foundation under Grant no. CCR.-9005992 and in part by the Semiconductor Research Corporation under Contract 92-DJ-294 and in part by the U.S.-Israeli Binational Science Foundation and in part by a Japan-U.S. cooperative research grant from the Japanese Society for the Promotion of Scientific Research and in part by U.S.-Japan cooperative research grant number INT-90-16694 from the National Science Foundation.
The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the U.S. government.
Rights and permissions
About this article
Cite this article
Clarke, E.M., Grumberg, O., Hiraishi, H. et al. Verification of the Futurebus+ cache coherence protocol. Form Method Syst Des 6, 217–232 (1995). https://doi.org/10.1007/BF01383968
Issue date:
DOI: https://doi.org/10.1007/BF01383968