## 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