Reference:

Mark D. Aagaard, Byron Cook, Nancy A. Day, and Robert B. Jones. A framework for microprocessor correctness statements. In Tiziana Margaria and Tom Melham, editors, Correct Hardware Design and Verification Methods ({CHARME} '01), volume 2144 of Lecture Notes in Computer Science, pages 433-448. Springer-Verlag, September 2001.

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.

Download (please read copyright notice):

PostScript (gzipped)
PDF

BibTeX entry:

@InProceedings{AagaardEtal01Charme,
  author    = {Mark D. Aagaard and 
               Byron Cook and
               Nancy A. Day and
               Robert B. Jones},
  title     = {A Framework for Microprocessor Correctness Statements},
  booktitle = {Correct Hardware Design and Verification Methods ({CHARME} '01)},
  pages     = {433--448},
  editor    = {Tiziana Margaria and Tom Melham},
  volume    = 2144,
  series    = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  month     = {September},
  year      = 2001,
}