Enhancing SAT-based Bounded Model Checking using sequential logic implications
Rajat Arora, Michael S. Hsiao · 2004
We present a novel technique of improving the SAT-based Bounded Model Checking, by inducing powerful sequential signal correlations (crossing time-frame boundaries) into the original CNF formula of the unrolled circuit. A quick preprocessing on the circuit-under-verification, builds a large set of direct and indirect sequential implications. The non-trivial implications (spanning multiple time-frames) are converted into two-literal clauses. These clauses are quickly replicated throughout the unrolled sequential circuit, and appended to the existing CNF database. The added clauses prune the overall search space of SAT-solver engine and provide correlation among the different variables, which enhances the Boolean Constraint Propagation (BCP). Experimental Results for checking difficult instances of random safety properties on ISCAS'89 benchmark circuits show that more than 148x speedup can be achieved over the conventional approach.