Reference:

Jens U. Skakkebæk, Robert B. Jones, and David L. Dill. Formal verification of out-of-order execution using incremental flushing. In Alan J. Hu and Moshe Y. Vardi, editors, Computer-Aided Verification (CAV), volume 1427 of Lecture Notes in Computer Science, pages 98-109. Springer-Verlag, June-July 1998.

Abstract:

We present a two-part approach for verifying out-of-order execution. First, the complexity of out-of-order issue and scheduling is handled by creating an in-order abstraction of the out-of-order execution core. Second, incremental flushing addresses the complexity difficulties encountered by automated abstraction functions on very deep pipelines. We illustrate the techniques on a model of a simple out-of-order processor core.

Download (please read copyright notice):

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

BibTeX entry:

@InProceedings{SkJonesDill98CAV,
  author    = {Jens U. Skakkeb{\ae}k and 
               Robert B. Jones and 
               David L. Dill},
  title     = {Formal Verification of Out-of-Order Execution 
               Using Incremental Flushing},
  pages     = {98-109},
  booktitle = {Computer-Aided Verification (CAV)},
  editor    = {Alan~J. Hu and Moshe~Y. Vardi},
  volume    = 1427,
  series    = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  month     = {June-July},
  year      = 1998,
}