Formal specification combined with mechanical verification is a promising approach for achieving the extremely high levels of assurance required of safety-critical digital systems. However. many questions remain regarding their use in practice: Can these techniques scale up to industrial systems, where are they likely to be useful. and how should industry go about incorporating them into practice? This report discusses a project undertaken to answer some of these questions, the formal verification of the AA11PS microprocessor. This project consisted of formally specifying in the PVS language a Rockwell proprietary microprocessor at both the instruction set and register-transfer levels and using the PVS theorem prover to show that the microcode correctly implemented the instruction-level specification for a representative subset of instructions, Notable aspects of this project include the use of a formal specification language by practicing hardware and software engineers. the integration of traditional inspections with formal specifications. and the use of a mechanical theorem prover to verify a portion of a commercial, pipelined microprocessor that was not explicitly designed for formal verification,

• csl-95-4.ps