## Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions

journal contribution

posted on 01.01.1998, 00:00 by Randal E. Bryant, Steven German, Miroslav N VelevIn using the logic of equality with unininterpreted functions to verify
hardware systems, specific characteristics of the formula describing the correctness
condition can be exploited when deciding its validity. We distinguish
a class of terms we call “p-terms” for which equality comparisons can appear
only 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 a procedure that translates the original formula
into one in propositional logic by interpreting the formula over a domain
of fixed-length bit vectors and using vectors of propositional variables to encode
domain variables. By exploiting maximal diversity, this procedure can greatly
reduce the number of propositional variables that must be introduced.
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 [VB98] when verifying microprocessors with load, store,
and branch instructions.