Microcode verification using SDVS-the method and a case study

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.