Reference:

Robert B. Jones, Jens U. Skakkebæk, and David L. Dill. Formal verification of out-of-order execution with incremental flushing. Formal Methods in System Design, Special Issue on Microprocessor Verification, 20(2):139-158, March 2002.

Abstract:

We present an approach for formally verifying that a high-level microprocessor model behaves as defined by an instruction-set architecture. The technique is based on a specialization of self consistency called incremental flushing and reduces the need and effort required to create manually-generated intermediate abstractions. Additionally, incremental flushing reduces the computational complexity of the proof obligations generated when reasoning about out-of-order execution. This is accomplished by comparing the functional behavior of a slightly-modified implementation over two sets of inputs: one that represents normal operation and one that is simpler, but functionally equivalent. The approach is illustrated on a simple out-of-order microprocessor core.

Download (please read copyright notice):

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

BibTeX entry:

@Article{JonesSkDill02FMSD,
  author    = {Robert B. Jones and 
               Jens U. Skakkeb{\ae}k and 
               David L. Dill},
  title     = {Formal Verification of Out-of-Order Execution 
               with Incremental Flushing},
  journal   = {Formal Methods in System Design, 
               Special Issue on Microprocessor Verification},
  editor    = {Warren A. Hunt~Jr.},
  publisher = {Kluwer Academic Publishers},
  volume    = 20,
  number    = 2,
  month     = mar,
  year      = 2002,
  pages     = {139--158},
}