Symbolic model checking using SAT procedures instead of BDDs

TLDR

The study investigates using propositional decision procedures for hardware verification and proposes optimizations to reduce propositional formula size. The authors apply bounded model checking with propositional decision procedures, optimizing the generated formulas for equivalence and invariant checking. The SAT-based approach significantly outperforms BDD-based methods and efficiently detects errors in both combinational and sequential designs.

Abstract

In this paper, we study the application of propositional decision procedures in hardware verification. In particular, we apply bounded model checking to equivalence and invariant checking. We present several optimizations that reduce the size of generated propositional formulas. In many instances, our SAT-based approach can significantly outperform BDD-based approaches. We observe that SAT-based techniques are particularly efficient in detecting errors in both combinational and sequential designs.