Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions

We present a collection of ideas that allows the pipeline verification method pioneered by Burch and Dill [5] to scale very efficiently to dual-issue superscalar processors. We achieve a significant speedup in the verification of such processors, compared to the result by Burch [6], while using an entirely automatic tool. Instrumental to our success are exploiting the properties of positive equality [3][4] and the simplification capabilities of BDDs.