Verification of the Futurebus+ Cache Coherence Protocol**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.
Elsevier eBooksPublished 1 January 1993
Edmund M. Clarke, Orna Grümberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan
Citations102
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
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.
Keywords
Computer ScienceEngineering
IEEE Transactions on ComputersGraph-Based Algorithms for Boolean Function Manipulation
8,829 Citations1986Bryant
Experimental results from applying a new data structure for representing Boolean functions and an associated set of manipulation algorithms to problems in logic design verification demonstrate the practicality of this approach.
ACM Transactions on Programming Languages and SystemsAutomatic verification of finite-state concurrent systems using temporal logic specifications
3,555 Citations1986E. M. Clarke, E. Allen Emerson +1 more
It is argued that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems.
Lecture notes in computer scienceSpecification and verification of concurrent systems in CESAR
1,277 Citations1982J. P. Queille, Joseph Sifakis
By an example, the alternating bit protocol, the use of CESAR, an interactive system for aiding the design of distributed applications, is illustrated.
Theoretical Computer ScienceThe temporal semantics of concurrent programs
701 Citations1981Amir Pnueli
It is demonstrated that specification of the Temporal character of the program's behavior is absolutely essential for the unambiguous understanding of the meaning of programming constructs.
Sequential circuit verification using symbolic model checking
409 Citations1990Jerry R. Burch, E. M. Clarke +2 more
Symbolic Model Checking
258 Citations1993Kenneth L. McMillan
Representing circuits more efficiently in symbolic model checking
176 Citations1991Jerry R. Burch, E. M. Clarke +1 more
This work significantly reduces the complexity of BDD-based symbolic verification by using partitioned transition relations to represent state transition graphs and was able to handle example pipelines with over l O l Z o reachable states.