
VERIFYING OUTOFORDER EXECUTIONSAbstractWe present an approach to the specification and verification of outoforder execution in the design of microprocessors. Ultimately, the appropriate statement of correctness is that the outoforder 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 outoforder 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 outoforder 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 modelchecking approaches). Our proof method is based on refinement (proved by simulation) for comparing the outoforder 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 outoforder 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 outoforder design with the reference model. If time permits, we will also sketch an alternative algorithmic approach to verifying outoforder executions, based on the notion of Herbrand Automata. This work was jointly done with W. Damm
Relevant PapersW. Damm and A. Pnueli, "Verifying OutofOrder Executions", Charme97

Contact 
©20022018 U.C. Regents 