Formal Verification of Superscalar Microprocessors with Multicycle Functional Units, Exceptions, and Branch Prediction
journal contributionposted on 2005-07-01, 00:00 authored by Miroslav N Velev, Randal E. Bryant
We extend the Burch and Dill flushing technique  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 . We study the modeling of the above features in different versions of dual-issue superscalar processors.