Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic
journal contributionposted on 2007-01-01, 00:00 authored by Miroslav N Velev, Randal E. Bryant
We present a collection of ideas that allows the pipeline verification method pioneered by Burch and Dill  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 , while using an entirely automatic tool. Instrumental to our success are exploiting the properties of positive equality  and the simplification capabilities of BDDs.