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 1974
Conference paper
Procedure for testing microprograms
Abstract
To produce reliable, i.e. defect-free microprograms a two phase procedure is recommended. The first phase consists of expressing the desired algorithms in a precise formal way employing a suitable specification language so that the 'correctness' of the specifications can be examined. The second phase consists of transcribing these specifications into machine code microprograms and proving the 'equivalence' between the formal specifications and the machine microcodes. Various desiderata of such a specification language are described and the reasons supporting each are given. Several uses for an implemented version are advocated and all depend on the 'correctness' of the implementation. Unique means for thoroughly checking the programmed implementation are given and the possibility of mathematically proving it correct is discussed.