Formal Verification of Iterative Algorithms in Microprocessors

Contemporary microprocessors implement many iterative algo-rithms. For example, the front-end of a microprocessor repeat-edly fetches and decodes instructions while updating internal state such as the program counter; floating-point circuits perform di-vide and square-root computations iteratively. Circuit implemen-tations of iterative algorithms are often complex because of per-formance optimizations such as result speculation, re-timing and circuit redundancies. Verifying circuits that implement iterative al-gorithms against high-level specifications requires two steps: rea-soning 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 ver-ification system; we discuss the Forte features necessary for our approach. 1