Formal Verification of Out-of-Order Execution Using Incremental Flushing
Jens U. Skakkebaek, Robert B. Jones, David L. Dill · 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 abstrac-tion functions on very deep pipelines. We illustrate the techniques on a model of a simple out-of-order processor core. 1