Utilizing don't care states in SAT-based bounded sequential problems

Boolean Satisfiability (SAT) solvers are popular engines used throughout the verification world. Bounded sequential problems such as bounded model checking and bounded sequential equivalence checking rely on fast and robust SAT solvers. In this work, we introduce a technique that improves the performance of the underlying SAT solver for bounded sequential problems by taking advantage of a design’s don’t care states. We develop cost effective methods of filtering, replicating and applying the don’t care states to the original problem thus reducing the search space. Experiments demonstrate the effectiveness of the proposed method on ISCAS’89 benchmarks. Categories and Subject Descriptors J.6 [Computer-Aided Engineering]: Computer-aided design (CAD) General Terms Algorithms, Performance, Verification Keywords Don’t Care States, Satisfiability, Bounded Model Checking, Sequential Equivalence Checking, Unreachable States

• Type: Conference
• Year: 2005
• Where: GLVLSI
• Authors: Sean Safarpour, Görschwin Fey, Andreas G. Veneris, Rolf Drechsler
• Keywords: Care States, GLVLSI 2005, Sequential Equivalence, Sequential Problems, VLSI