Title :
Combining theorem proving and trajectory evaluation in an industrial environment
Author :
Aagaard, Mark D. ; Jones, Robert B. ; Sege, Carl-Johan H.
Author_Institution :
Strategic CAD Labs., Intel Corp., Hillsboro, OR, USA
Abstract :
We describe the verification of the IM: a large, complex (12000 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 model-checking 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.
Keywords :
formal verification; instruction sets; logic testing; theorem proving; IM; Intel architecture; gate-level model; instruction sets; model-checking runs; theorem proving; trajectory evaluation; Circuits; Computer bugs; Decoding; Design optimization; Hardware; Latches; Permission; Phase detection; Timing; Writing;
Conference_Titel :
Design Automation Conference, 1998. Proceedings
Conference_Location :
San Francisco, CA, USA
Print_ISBN :
0-89791-964-5
