Combining theorem proving and trajectory evaluation in an industrial environment
Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger · 1998
We describe the verification of the IM: a large, complex (12,000gates and 1100 latches) circuit that detects and marks the boundariesbetween Intel architecture (IA-32) instructions. We verified agate-level model of the IM against an implementation-independentspecification of IA-32 instruction lengths. We used theorem provingto to derive 56 model-checking runs and to verify that the model-checkingruns imply that the IM meets the specification for all possiblesequences of IA-32 instructions. Our verification discoveredeight previously unknown bugs.