Reference:

Mark D. Aagaard, Robert B. Jones, and Carl-Johan H. Seger. Combining theorem proving and trajectory evaluation in an industrial environment. In Design Automation Conference (DAC), pages 538-541. ACM Press, June 1998.

Abstract:

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 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.

Download (please read copyright notice):

PostScript (gzipped)
PDF (auto-translated from PS, may have problems)

BibTeX entry:

@InProceedings{AagaardJonesSeger98DAC,
  author    = {Mark D. Aagaard and 
               Robert B. Jones and 
               Carl-Johan H. Seger},
  title     = {Combining Theorem Proving and Trajectory Evaluation
               in an Industrial Environment},
  pages     = {538--541},
  month     = {June},
  year      = 1998,
  booktitle = {Design Automation Conference (DAC)},
  publisher = {ACM Press},
}