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: 112-117
Randal E. Bryant , Carnegie Mellon University, Pittsburgh, PA
Miroslav N. Velev , Carnegie Mellon University, Pittsburgh, PA
ABSTRACT
We extend the Burch and Dill flushing technique [6] for formal verification of microprocessors to be applicable to designs where the functional units and memories have multicycle and possibly arbitrary latency. We also show ways to incorporate exceptions and branch prediction by exploiting the properties of the logic of Positive Equality with Uninterpreted Functions [4][5]. We study the modeling of the above features in different versions of dual-issue superscalar processors.
INDEX TERMS
fault modeling, fault simulation, hard faults, test vector generation
CITATION
Randal E. Bryant, Miroslav N. Velev, "Formal Verification of Superscale Microprocessors with Multicycle Functional Units, Exception, and Branch Prediction", Design Automation Conference, vol. 00, no. , pp. 112-117, 2000, doi:10.1109/DAC.2000.855288
96 ms
(Ver )