file.pdf (131.54 kB)
Download file

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