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

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 der 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.

• Type: Conference
• Year: 1998
• Where: CAV
• Authors: Jens U. Skakkebæk, Robert B. Jones, David L. Dill
• Keywords: Automated Abstraction Functions, CAV 1998, Hardware, Out-of-order Execution, Out-of-order Execution Core