Verifying out-of-order executions

摘要

The paper presents an approach to the specification and verification of out-of-order execution in the design of micro-processors. Ultimately, the appropriate statement of correctness is that the out-of-order execution produces the same final state as a purely sequential machine running the same program.