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