A Framework for Microprocessor Correctness Statements

Mark D. Aagaard, Byron Cook, Nancy A. Day, and Robert B. Jones

In CHARME 2001, Livingston, Scotland, Sept 4-7, 2001.

Abstract
Paper (gzipped postscript)
Bibtex entry


Abstract

Most verifications of out-of-order microprocessors compare state-machine-based implementations and specifications, where the specification is based on the instruction-set architecture. The different efforts use a variety of correctness statements, implementations, and verification approaches. We present a framework for classifying correctness statements about safety that is independent of implementation representation and verification approach. We characterize the relationships between the different statements and illustrate how existing and classical approaches fit within this framework.

Bibtex Entry

@INPROCEEDINGS{AoCoDaJo01,
  title={A Framework for Microprocessor Correctness Statements},
  booktitle = {Advanced Research Working Conference
     on Correct Hardware Design and Verification Methods (CHARME)}
  year = 2001,
  series={Lecture Notes in Computer Science},
  volume = 2144,
  publisher={Springer}
  pages = {433--448},
  editors = {T. Margaria and T. Melham}
}

Send questions or comments to Mark Aagaard < markaa@swen.uwaterloo.ca >