file.pdf (131.54 kB)
Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic
journal contribution
posted on 2007-01-01, 00:00 authored by Miroslav N Velev, Randal E. BryantWe 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.