DLX

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.

[an error occurred while processing this directive]

Abstract State Machines