Formal Verification of Out-of-Order Execution Using Incremental Flushing

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.

Document type: Part of book or chapter of book

Full document

Original document

The different versions of the original document can be found in:

• http://dx.doi.org/10.21236/ada400401

• http://www.dtic.mil/get-tr-doc/pdf?AD%3DADA400401

• https://link.springer.com/content/pdf/10.1007%2FBFb0028737.pdf

DOIS: 10.21236/ada400401 10.1007/bfb0028737