# Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions

journal contribution

posted on 01.01.2006, 00:00 by Randal E. Bryant, Steven German, Miroslav N VelevModern processors have relatively simple specificationsbased on their
instruction set architectures. Their implementations, however, are very complex,
especially with the advent of performance-enhancing techniques such as pipelining,
superscalar operation, and speculative execution. Formal techniques to verify
that a processor implements its instruction set specification could yield more
reliable results at a lower cost than the current simulation-based verification techniques
used in industry.
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. Using a method devised by Burch and Dill [BD94], the
correctness of a processor can be inferred by deciding the validity of a formula
in EUF describing the comparative effect of running one clock cycle of processor
operation to that of executing a small number (based on the processor issue rate)
of machine instructions.
This paper describes recent advances in reducing formulas in EUF to propositional
logic. We can then use either Binary Decision Diagrams (BDDs) or satisfiability
procedures to determine whether this propositional formula is a tautology.
We can exploit characteristics of the formulas generated when modeling
processors to significantly reduce the number of propositional variables, and consequently
the complexity, of the verification task.