Predicate abstraction and refinement techniques for verifying Verilog

Abstract: "Model checking techniques applied to large industrial circuits suffer from the state explosion problem. A major technique to address this problem is abstraction. Predicate abstraction has been applied successfully to large software programs. Applying this technique to hardware designs poses additional challenges. This paper evaluates three techniques to improve the performance of SAT-based predicate abstraction of circuits: 1) We partition the abstraction problem by forming subsets of the predicates. The resulting abstractions are more coarse, but the computation of the abstract transition relation becomes easier. 2) We evaluate the performance effect of lazy abstraction, i.e., the abstraction is only performed if required by a spurious counterexample. 3) We use weakest preconditions of circuit transitions in order to obtain new predicates during refinement. We provide experimental results on publicly available benchmarks from the Texas97 benchmark suite.