Sciweavers

DAC
2000
ACM

Formal verification of iterative algorithms in microprocessors

14 years 4 months ago
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.
Mark Aagaard, Robert B. Jones, Roope Kaivola, Kath
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 2000
Where DAC
Authors Mark Aagaard, Robert B. Jones, Roope Kaivola, Katherine R. Kohatsu, Carl-Johan H. Seger
Comments (0)