EECS 298-11: Special CAD Seminar Monday, February 26, 1995, 2pm Cory Hall--Wang Room A formal specification and a correctness proof for pipelining in RISC architectures Egon Boerger Dipartimento di Informatica, Universita di Pisa (Italy) on sabbatical leave at Siemens R&D, Munich (Germany) We provide a formal specification of Hennessy's and Patterson's RISC processor DLX and prove the correctness of its pipelined model with respect to the sequential ground model. Our specification proceeds by stepwise refinement, the proof method is modular. In the first part we develop a provably correct refinement of the sequential ground model DLX to the pipelined parallel version DLXp in which structural hazards are eliminated. Then we extend the result to a model DLXdata and finally to the full pipelined model DLXpipe in which also data and control hazards are treated. The specification and verification method uses Gurevich's concept of evolving algebras. It is general and can be applied to other microprocessors and pipelining techniques as well. (Joint work with S. Mazzanti) Upcoming Seminars: 2/28/96: Ramin Hojati, UC Berkeley 3/6/96: Steve McGeady, Intel Internet Technology Lab 3/13/96: Yogen Dalal, Mayfield Fund