Microcode Verification Project.

The goal of the microcode verification project at ISI is the development of both the theory and tools for verification of microcode. The strategy has been to push the development of a working system, letting the theoretical issues and the human engineering questions emerge during system development. The ISPS language is used for encoding our machine descriptions. The State Delta formalism is used for reasoning about the course of the computation. A system to check proofs of microcode validity is currently built. The system is composed of a data base and simplifier that perform some automatic deductions to make checking of the proofsteps manageable, as well as a proof language and a user interface. A particular computer the FTSC is used to establish a focus for the project and to provide a source of examples. This document reports the results of verifying the microcode of the square root instruction of the FTSC, and the results of verifying the complete microcode of a much smaller fictitious example machine.