Microcode verification using SDVS-the method and a case study
B. H. Levy · ACM SIGMICRO newsletter/SIGMICRO newsletter/SIGMICRO, TCMICRO newsletter · 1984
This paper describes SDVS (State Delta Verification System), its application to microcode verification, and the verification of a particular example referred to as the H-machine example. The example illustrates how particular microcode that interprets a computer instruction set can be proved correct and how this proof is accomplished with an existing, automated verification system.