Reference:

Mark D. Aagaard, Robert B. Jones, Roope Kaivola, Katherine R. Kohatsu, and Carl-Johan H. Seger. Formal verification of iterative algorithms in microprocessors. In Design Automation Conference (DAC), pages 201-206. ACM Press, June 2000.

Abstract:

Contemporary microprocessors implement many iterative algorithms. For example, the front-end of a microprocessor repeatedly fetches and decodes instructions while updating internal state such as the program counter; floating-point circuits perform divide and square-root computations iteratively. Circuit implementations of iterative algorithms are often complex because of performance optimizations such as result speculation, re-timing and circuit redundancies. Verifying circuits that implement iterative algorithms against high-level specifications requires two steps: reasoning about the algorithm itself and verifying the implementation against the algorithm. We discuss the verification of four iterative circuits from Intel microprocessor designs and how these proofs were maintained in the face of evolving design implementations. These verifications were performed using Forte, a custom-built verification system; we discuss the Forte features necessary for our approach.

Download (please read copyright notice):

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

BibTeX entry:

@InProceedings{AagaardEtal00DAC,
  author    = {Mark D. Aagaard and 
               Robert B. Jones and
               Roope Kaivola and
               Katherine R. Kohatsu and
               Carl-Johan H. Seger},
  title     = {Formal Verification of Iterative Algorithms in Microprocessors},
  pages     = {201--206},
  month     = {June},
  year      = 2000,
  booktitle = {Design Automation Conference (DAC)},
  publisher = {ACM Press},
}