SAT-Based Scalable Formal Verification Solutions

Functional Verification has become an important aspect of the design process. Significant resources, both in industry and academia, are devoted to bridging the gap between design complexity and verification efforts. This book provides an engineering insight into how to provide a scalable and robust verification solution with ever increasing design complexity and sizes. With growing interests in SAT-based approaches for formal verification and increasing dissatisfaction twoard BDD-based approaches, this book brings together the various SAT-based scalable emerging technologies. Though the approaches described in the book are based on well-founded mathematics, the discussion is generally restricted to the engineering aspect for the ease of readability. Readers will also be exposed to the specific strengths of the various approaches in regard to the applicability.

Describes SAT-based model checking approaches and gives engineering details on what makes model checking practical Techniques covered can be synergistically combined into a scalabe solution Focuses on engineering design and not mathematics Includes supplementary material: sn.pub/extras

Contenu
Design Verification Challenges.- Design Verification Challenges.- Background.- Basic Infrastructure.- Efficient Boolean Representation.- Hybrid DPLL-Style SAT Solver.- Falsification.- SAT-Based Bounded Model Checking.- Distributed SAT-Based BMC.- Efficient Memory Modeling in BMC.- BMC for Multi-Clock Systems.- Proof Methods.- Proof by Induction.- Unbounded Model Checking.- Abstraction/Refinement.- Proof-Based Iterative Abstraction.- Verification Procedure.- SAT-Based Verification Framework.- Synthesis for Verification.