file.pdf (79.48 kB)
Download file

Formal Verification of Superscalar Microprocessors with Multicycle Functional Units, Exceptions, and Branch Prediction

Download (79.48 kB)
journal contribution
posted on 01.07.2005, 00:00 authored by Miroslav N Velev, Randal E. Bryant
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 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.




Usage metrics