Incremental deductive & inductive reasoning for SAT-based Bounded Model Checking

Bounded Model Checking (BMC) based on Boolean Satisfiability (SAT) methods has recently gained popularity as a viable alternative to BDD-based techniques for verifying large designs. This work proposes a number of conceptually simple, but extremely effective, optimizations for enhancing the performance of SAT-based BMC flows. The keys ideas include (1) a novel idea to combine SAT-based inductive reasoning and BMC, (2) clever orchestration of variable ordering and learned information in an incremental framework for BMC, and (3) BMC-specific ordering strategies for the SAT solver. Our experiments, conducted on a wide range of industrial designs, show that the proposed optimizations consistently provide between 1-2 orders of magnitude speedup and can be extremely useful in enhancing the efficacy of typical SAT-BMC tools.