Automatic Refinement Checking of Pipelines with Out-of-Order Execution

We show how to automatically verify pipelined machines with out-of-order execution using refinement. Our notion of refinement is based on Well-Founded Equivalence Bisimulations. Proving refinement guarantees that a pipelined machine will preserve all safety and liveness properties of its instruction set architecture. Checking liveness—used to ensure that deadlocks do not occur, i.e., there is always forward progress—is essential for out-of-order machines as the control logic is involved and prone to deadlock defects. In previous work on out-of-order verification, liveness checking was either ignored or not automated. We developed two automatic methods based on refinement that check both safety and liveness of out-of-order pipelined machines. We use extensive experimentation based on 14 out-of-order machine models to study and compare these methods. We find overall that the cost of proving both safety and liveness is about 81 percent more than the cost of proving safety alone.