file.pdf (79.48 kB)
Formal Verification of Superscalar Microprocessors with Multicycle Functional Units, Exceptions, and Branch Prediction
journal contribution
posted on 2005-07-01, 00:00 authored by Miroslav N Velev, Randal E. BryantWe 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 multi-cycle 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.