About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
MICRO Annual Workshop 1976
Conference paper
Automated proofs of microprogram correctness
Abstract
This paper presents a method for verifying microprograms with computer aid, and examples of its application to actual systems. The specifications for an architecture and those for the computer on which it is to be implemented are both described formally, with the microcode supplied as data to the low level description, A correspondence between the two descriptions is then formalized, and a system of programs is used to prove mathematically that the correspondence holds. This interactive, goal-directed system not only provides a proof that microcode performs as specified, but more often aids in detecting and correcting microprogram errors. Several errors in actual implementations, some of which were difficult to detect using test cases,have been discovered in this way.