BDD Based Procedures for a Theory of Equality with Uninterpreted Functions

. The logic of equality with uninterpreted functions has been proposed for verifying abstract hardware designs. The ability to perform fast satisfiability checking over this logic is imperative for this verification paradigm to be successful. We present symbolic methods for satisfiability checking for this logic. The first procedure is based on restricting analysis to finite instantiations of the design. The second procedure directly reasons about equality by introducing Boolean-valued indicator variables for equality. Theoretical and experimental evidence shows the superiority of the second approach. 1 Verifying High-level Designs Using the Theory of Equality A common problem with automatic formal verification is that the computational resources required for verification increase rapidly with the size of the design. Stateof -the art tools for verification of gate-level designs are not capable of routinely verifying designs possessing more than a hundred to two hundred binary-valued l..