INCREMENTAL DESIGN AND FORMAL VERIFICATION OF MICROCODED MICROPROCESSORS

A number of microprocessors have been specified and verified using machine supported formal techniques [2], [1], [7], [8], [10]. Some of these were pre-existing designs, others were designed as part of the specification and verification project. Even in the case of new designs, the formal techniques used offered very little support for incremental design and verification. Support for incremental design and verification means that certain additions to the implementation and/or specification can be verified without re-verification of the previous parts. Here, we present techniques for incremental design and verification which, as well as providing more appropriate models, also make the formal verification more efficient. The formal framework to support these ideas has been implemented in the HOL system and has been used in the specification, design and verification of a microcoded microprocessor. The techniques deal with three different aspects of the microprocessor: specification of machine instructions, modelling of microcode and modelling of bus architecture. For each of these, the techniques support incremental design and verification.