Reference:

Mark D. Aagaard, Byron Cook, Nancy A. Day, and Robert B. Jones. A framework for superscalar microprocessor correctness statements. Software Tools for Technology Transfer, 4(3):298-312, 2003. (on-line publication was in 2002).

Abstract:

Most verifications of superscalar, out-of-order microprocessors compare state-mach\-ine-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. Our framework is independent of the implementation representation and verification approach, and is parameterized by the width of the processor. We characterize the relationships between the correctness statements of many different efforts and also illustrate how classical approaches fit within our framework.

Download (please read copyright notice):

PostScript (gzipped)
PDF (auto-translated from PS, may have problems)

BibTeX entry:

@Article{AagaardEtal03STTT,
  author    = {Mark D. Aagaard and 
               Byron Cook and
               Nancy A. Day and
               Robert B. Jones},
  title     = {A Framework for Superscalar Microprocessor 
               Correctness Statements},
  journal   = {Software Tools for Technology Transfer},
  editor    = {Tiziana Margaria},
  publisher = {Springer-Verlag},
  volume    = 4,
  number    = 3,
  pages     = {298--312},
  year      = 2003,
  note      = {(on-line publication was in 2002)},
}