Verification of the Futurebus+ Cache Coherence Protocol

Abstract

We used a hardware description language to construct a formal model of the cache coherence protocol described in the draft IEEE Futurebus+ standard. By applying temporal logic m odel checking techniques, we found several errors in thee standard. Thee 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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1992
Accession Number
ADA259075

Entities

People

  • Daniel Long
  • E. Clarke
  • H. Hiraishi
  • K. Mcmillan
  • L. Ness
  • O. Grumberg
  • Shalini Jha

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Advanced Electronics
  • Energy and Power Technologies
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Air Force
  • Algorithms
  • Communication Systems
  • Communications Protocols
  • Complex Systems
  • Computations
  • Computer Science
  • Debugging
  • Formal Languages
  • Language
  • Scientific Research
  • Specifications
  • Standards
  • Transitions
  • Verification

Fields of Study

  • Computer science

Readers

  • Parallel and Distributed Computing.
  • Software Engineering.
  • Systems Analysis and Design