DIMACS TR: 96-22

A Correctness Proof for Pipelining in RISC Architecture



Authors: E. Boerger and S. Mazzanti

ABSTRACT

We describe a technique for specifying and verifying the control of pipelined microprocessors which can be used where traditional or purely automatic methods do not scale up to complex commercial microprocessor design. We illustrate our approach through a formal specification of Hennessy's and Patterson's RISC processor DLX for which we prove the correctness of its pipelined model with respect to the sequential model.

First we concentrate our attention on the provably correct refinement of the sequential ground model DLX to the pipelined parallel version DLX_p in which structural hazards (resource conflicts) are eliminated. Then we extend the result to the model DLX_data in which also data hazards for not jump instructions are treated. The next step consists of building the model DLX_control in which control hazards are eliminated. In the last step we define DLX_pipe and prove that it refines DLX_control correctly and takes care also of data hazards relative to jump instructions.

Due to the systematic use of successive refinements, which are organized around the different pipelining problems and the methods for their solution, our approach can be applied for the design-driven verification as well as for the verification-driven design of RISC cores at any level of abstraction. The proof method supports the designer's intuitive reasoning; ``local'' argumentations, which are typical for incremental design and for optimizations, are supported by the semantical modularity of the design and proof method. The specification method supports the descriptive part of the designer's actual work; it is general and can be applied to other microprocessors and pipelining techniques as well. Since our models come in the form of evolving algebras, they can be made executable by evolving algebra interpreters and can thereby be used for (prototypical) simulations.

NOTE: The first author wants to express his thanks to $DIMACS$ for the hospitality during the Fall of 1995 when part of this work was done.

Paper Available at: ftp://dimacs.rutgers.edu/pub/dimacs/TechnicalReports/TechReports/1996/96-22.ps.gz


DIMACS Home Page