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.