Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment

We describe the verification of the IM: a large, complex (12,000 gates and 1100 latches) circuit that detects and marks the boundaries between Intel architecture (IA-32) instructions. We verified a gate-level model of the IM against an implementation-independent specification of IA-32 instruction lengths. We used theorem proving to to derive 56 modelchecking runs and to verify that the model-checking runs imply that the IM meets the specification for all possible sequences of IA-32 instructions. Our verification discovered eight previously unknown bugs.

• Type: Conference
• Year: 1998
• Where: DAC
• Authors: Mark Aagaard, Robert B. Jones, Carl-Johan H. Seger
• Keywords: DAC 1998, Design Automation, Implementation-independent Specification, Instruction Lengths, Unknown Bugs