SMT(CLU): A Step toward Scalability in System Verification

We describe a SAT-based decision method for the underlying logic in many formal verification problems; i.e. the counter arithmetic logic with lambda expressions and uninterpreted functions (CLU). This logic is well suited for equivalence checking of two versions of a hardware design or the input and output of a compiler and has been recently utilized in several model checkers. Our method follows the general satisfiability modulo theories or SMT(T) framework and combines a DPLL-style SAT solver with two theory solvers; one specific to equality and the other to separation inequality atoms within CLU. By adopting a combined implication scheme, we coordinate the efforts among theory solvers, and by efficiently processing uninterpreted functions involved in conflicts, we considerably improve the effectiveness of SAT learning and backtracking routines. Finally, we empirically demonstrate the effectiveness of our SMT(CLU) procedure and compare its performance to recent solvers on a wide range of hardware verification benchmarks