Sciweavers

DAC
1998
ACM

Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment

14 years 4 months ago
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.
Mark Aagaard, Robert B. Jones, Carl-Johan H. Seger
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 1998
Where DAC
Authors Mark Aagaard, Robert B. Jones, Carl-Johan H. Seger
Comments (0)