Computer Science Department
School of Computer Science, Carnegie Mellon University
Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic
Randal E. Bryant, Steven German*, Miroslav N. Velev
We can exploit characteristics of the formulas describing the verification conditions to greatly simplify the propositional formulas generated. We identify a class of terms we call "p-terms" for which equality comparisons can only be used in monotonically positive formulas. By applying suitable abstractions to the hardware model, we can express the functionality of data values and instruction addresses flowing through an instruction pipeline with p-terms. A decision procedure can exploit the restricted uses of p-terms by considering only "maximally diverse" interpretations of the associated function symbols, where every function application yields a different value except when constrained by functional consistency.
We present two methods to translate formulas in EUF into propositional logic. The first interprets the formula over a domain of fixed-length bit vectors and uses vectors of propositional variables to encode domain variables. The second generates formulas encoding the conditions under which pairs of terms have equal valuations, introducing propositional variables to encode the equality relations between pairs of terms. Both of these approaches can exploit maximal diversity to greatly reduce the number of propositional variables that need to be introduced and to reduce the overall formula sizes.
We present experimental results demonstrating the efficiency of this approach when verifying pipelined processors using the method proposed by Burch and Dill. Exploiting positive equality allows us to overcome the exponential blow-up experienced previously when verifying microprocessors with load, store, and branch instructions.
*IBM T.J. Watson Research Center, Yorktown Heights, New York.