Formal verification of iterative algorithms in microprocessors

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.

• Type: Conference
• Year: 2000
• Where: DAC
• Authors: Mark Aagaard, Robert B. Jones, Roope Kaivola, Katherine R. Kohatsu, Carl-Johan H. Seger
• Keywords: Circuits Perform Divide, DAC 2000, Design Automation, Iterative Algorithms, Iterative Circuits