A general method is presented for formally verifying the correctness of microprocessor designs. The abstract-level specification of the processor defines the effect of every instruction in terms of a suitably chosen programmer model of the processor. The concrete-level specification describes the design of the processor at a synchronous level by defining the behavior over a single microcycle. A general criterion of correctness to relate the two levels of behavior of the processor is developed. An application of the method to a simple processor, Simple, and a larger realistic processor, MiniCayuga, which uses instruction pipelining, is presented. Both designs are completely verified using an applicative-language-based verification system Clio. >