Carnegie Mellon University
file.pdf (131.54 kB)

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

Download (131.54 kB)
journal contribution
posted 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 [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.




Usage metrics