The Community for Technology Leaders
Design Automation Conference (2000)
Los Angeles, CA
June 5, 2000 to June 9, 2000
ISBN: 1-58113-1897-9
pp: 201-206
Mark D. Aagaard , Intel Corporation, Hillsboro, Oregon
Katherine R. Kohatsu , Intel Corporation, Hillsboro, Oregon
Roope Kaivola , Intel Corporation, Hillsboro, Oregon
Robert B. Jones , Intel Corporation, Hillsboro, Oregon
Carl-Johan H. Seger , Intel Corporation, Hillsboro, Oregon
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. Iterative algorithms often have complex implementations because of performance optimizations like result speculation, re-timing and circuit redundancies. Verifying these iterative circuits against high-level specifications requires two steps: reasoning about the algorithm itself and verifying the implementation against the algorithm. In this paper we discuss the verification of four iterative circuits from Intel microprocessor designs. These verifications were performed using Forte, a custom-built verification system; we discuss the Forte features necessary for our approach. Finally, we discuss how we maintained these proofs in the face of evolving design implementations.
INDEX TERMS
fault modeling, fault simulation, hard faults, test vector generation
CITATION
Mark D. Aagaard, Katherine R. Kohatsu, Roope Kaivola, Robert B. Jones, Carl-Johan H. Seger, "Formal Verification of Iterative Algorithms in Microprocessors", Design Automation Conference, vol. 00, no. , pp. 201-206, 2000, doi:10.1109/DAC.2000.855304
86 ms
(Ver 3.3 (11022016))