posted on 1978-01-01, 00:00authored byRandal E. Bryant, Steven German, Miroslav N Velev
The logic of Equality with Uninterpreted Functions (EUF) provides a means of abstracting the
manipulation of data by a processor when verifying the correctness of its control logic. By reducing
formulas in this logic to propositional formulas, we can apply Boolean methods such as ordered
Binary Decision Diagrams (BDDs) and Boolean satisfiability checkers to perform the verification.
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