Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic

Randal 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…