Enhancing SAT-based Bounded Model Checking using sequential logic implications

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.