Verification of a pipelined microprocessor using clio.

Clio is a system for verifying properties of expressions written in Caliban, a higher-order polymorphic strongly-typed lazy functional language akin to Turner's Miranda. Clio was designed for verifying each step in the implementation of a program: the specification, the high-level language, the assembly language, the microcode, and the hardware. This paper describes the use of Clio for verifying the correctness of an instruction pipelined microprocessor design. The abstract and the realization levels of behavior of the processor are modeled as infinite streams. The abstract specification describes the behavior in terms of a suitably chosen programmer's model of the processor. A realization specification gives a description of the design of the processor by describing the activities that happen in the circuit over a single microcycle. We develop a general criterion of correctness to relate the two levels which is verified using a form of fixed-point induction. [ABSTRACT FROM AUTHOR]