In the past we have verified a variety of different hardware circuits using different verification systems. In this paper we report on one such verification. The verification is that of a simple pipelined microprocessor first verified in [8]. We use this example as a vehicle for exploring a general methodology of verifying state machine systems in the PVS verification system. It is our hope that such a methodology can be extended to verify the correctness of actual commercial microprocessors.

• csl-93-12.ps