VERIFYING OUT-OF-ORDER EXECUTIONS

Abstract

We present 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 (and all relevant intermediate actions, such as writes to memory) as a purely sequential machine running the same program. The main methodology used is that of refinement and its proof by simulation. As a representative example, we verified the correctness of the Tomasulo algorithm for out-of-order execution, under some simplifying assumptions. The verification was carried out using deductive technology supported by the PVS theorem prover.

We will explain why we consider the problem of out-of-order execution an important and interesting problem and why we believe that it is a good candidate to be routinely solved by deductive techniques (rather than model-checking approaches).

Our proof method is based on refinement (proved by simulation) for comparing the out-of-order design with the reference model of sequential execution. The success of this approach hinges on a careful selection of the observable parts of the compared systems and on the introduction of an intermediate level specification which captures all the admissible out-of-order executions. It is argued that the deductive method is particularly appropriate for handling designs of such complexity since it can treat various design parameters, such as the number of functional units, the number of registers, etc. in a uniform way, providing a single proof for all values of these parameters. Another advantage of the approach is that it does not decompose the verification task into proofs of many small and partial properties, but establishes in one go the compatibility of the out-of-order design with the reference model.

If time permits, we will also sketch an alternative algorithmic approach to verifying out-of-order executions, based on the notion of Herbrand Automata.

This work was jointly done with W. Damm

Relevant Papers