Professor Pneuli will also be giving the Third Annual Milner Lecture on Wednesday 22 April.

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.

In a second part of the talk, we will sketch some approaches to the algorithmic verification of out-of-order designs based on the computational model of Herbrand Automata, which combines finite control with uninterpreted data registers and uninterpreted data operations. We will present an algorithm for deciding whether two Herbrand Automata of a certain limited class are equivalent.