Citation: Egon Börger and S. Mazzanti, "A Practical Method for Rigourously Controllable Hardware Design", in J.P. Bowen, M.G. Hinchey, D. Till, eds., ZUM'97: The Z Formal Specification Notation, Springer Lecture Notes in Computer Science 1212, 1997, 151--187.
Summary: The Hennessey and Patterson DLX pipelined microprocessor is specified by a series of successively refined ASMs, which are proved equivalent. The result is a formal proof of correctness for pipelining in the DLX microprocessor.
Subjects: Architectures, Hardware, Refinement, Verification
Download: PostScript, PDF, Compressed PostScript.
Notes: See also an earlier version of this paper.