| List of Figures | p. XIX |
| List of Tables | p. XXVII |
| Design Verification Challenges | p. 1 |
| Introduction | p. 1 |
| Simulation-based Verification | p. 1 |
| Formal Verification | p. 2 |
| Model Checking | p. 3 |
| Overview | p. 5 |
| Verification Tasks | p. 6 |
| Verification Challenges | p. 8 |
| Design Features | p. 8 |
| Verification Techniques | p. 9 |
| Verification Methodology | p. 11 |
| Organization of Book | p. 13 |
| Background | p. 17 |
| Model Checking | p. 17 |
| Correctness Properties | p. 18 |
| Explicit Model Checking | p. 19 |
| Symbolic Model Checking | p. 19 |
| Notations | p. 20 |
| Binary Decision Diagrams | p. 22 |
| Boolean Satisfiability Problem | p. 23 |
| Decision Engine | p. 25 |
| Deduction Engine | p. 26 |
| Diagnosis Engine | p. 28 |
| Proof of Unsatisfiability | p. 29 |
| Further Improvements | p. 30 |
| SAT-based Bounded Model Checking (BMC) | p. 32 |
| BMC formulation: Safety and Liveness Properties | p. 33 |
| Clocked LTL Specifications | p. 36 |
| SAT-based Unbounded Model Checking | p. 37 |
| SMT-based BMC | p. 39 |
| Notes | p. 40 |
| Basic Infrastructure | p. 41 |
| Efficient Boolean Representation | p. 43 |
| Introduction | p. 43 |
| Brief Survey of Boolean Representations | p. 45 |
| Extended Boolean Decision Diagrams (XBDDs) | p. 45 |
| Boolean Expression Diagrams (BEDs) | p. 45 |
| AND/INVERTER Graph (AIG) | p. 46 |
| Functional Hashing (Reduced AIG) | p. 49 |
| Three-Input Case | p. 50 |
| Four-Input Case | p. 52 |
| Example | p. 54 |
| Experiments | p. 57 |
| Simplification using External Constraints | p. 60 |
| Comparing Functional Hashing with BDD/SAT Sweeping | p. 61 |
| Summary | p. 62 |
| Notes | p. 62 |
| Hybrid DPLL-Style SAT Solver | p. 63 |
| Introduction | p. 63 |
| BCP on Circuit | p. 65 |
| Comparing CNF- and Circuit-based BCP Algorithms | p. 67 |
| Hybrid SAT Solver | p. 68 |
| Proof of Unsatisfiability | p. 69 |
| Comparison with Chaff | p. 69 |
| Applying Circuit-based Heuristics | p. 71 |
| Justification Frontier Heuristics | p. 71 |
| Implication Order | p. 72 |
| Gate Fanout Count | p. 73 |
| Learning XOR/MUX Gates | p. 74 |
| Verification Applications of Hybrid SAT Solver | p. 75 |
| Summary | p. 75 |
| Notes | p. 76 |
| Falsification | p. 77 |
| SAT-Based Bounded Model Checking | p. 79 |
| Introduction | p. 79 |
| Dynamic Circuit Simplification | p. 81 |
| Notation | p. 82 |
| Procedure Unroll | p. 83 |
| Comparing Implicit with Explicit Unrolling | p. 84 |
| SAT-based Incremental Learning and Simplification | p. 86 |
| BDD-based Learning | p. 90 |
| Basic Idea | p. 90 |
| Procedure: BDD_learning_engine | p. 91 |
| Seed Selection | p. 92 |
| Creation of BDDs | p. 93 |
| Generation of Learned Clauses | p. 94 |
| Integrating BDD Learning with a Hybrid SAT Solver | p. 95 |
| Adding Clauses Dynamically to a SAT Solver | p. 95 |
| Heuristics for Adding Learned Clauses | p. 96 |
| Application of BDD-based Learning | p. 97 |
| Customized Property Translation | p. 98 |
| Customized Translation for F(p) | p. 100 |
| Customized Translation of G(q) | p. 102 |
| Customized Translation of F(p[hat]G(q)) | p. 103 |
| Experiments | p. 104 |
| Comparative Study of Various Techniques | p. 105 |
| Effect of Customized Translation and Incremental Learning | p. 108 |
| Effect of BDD-based Learning on BMC | p. 109 |
| Static BDD Learning | p. 109 |
| Dynamic BDD Learning | p. 110 |
| Summary | p. 112 |
| Notes | p. 112 |
| Distributed SAT-Based BMC | p. 113 |
| Introduction | p. 113 |
| Distributed SAT-based BMC Procedure | p. 114 |
| Topology-cognizant Distributed-BCP | p. 116 |
| Causal-effect Order | p. 117 |
| Distributed-SAT | p. 118 |
| Tasks of the Master | p. 119 |
| Tasks of a Client C[subscript i] | p. 120 |
| SAT-based Distributed-BMC | p. 120 |
| Optimizations | p. 121 |
| Memory Optimizations in Distributed-SAT | p. 121 |
| Tight Estimation of Communication Overhead | p. 121 |
| Performance Optimizations in Distributed-SAT | p. 123 |
| Performance Optimization in SAT-based Distributed-BMC | p. 124 |
| Experiments | p. 124 |
| Related Work | p. 128 |
| Summary | p. 129 |
| Notes | p. 129 |
| Efficient Memory Modeling in BMC | p. 131 |
| Introduction | p. 131 |
| Basic Idea | p. 132 |
| Memory Semantics | p. 134 |
| EMM Approach | p. 135 |
| Efficient Representation of Memory Modeling Constraints | p. 136 |
| Comparison with ITE Representation | p. 139 |
| Non-uniform Initialization of Memory | p. 140 |
| EMM for Multiple Memories, Read, and Write Ports | p. 141 |
| Arbitrary Initial Memory State | p. 143 |
| Experiments on a Single Read/Write Port Memory | p. 144 |
| Experiments on Multi-Port Memories | p. 149 |
| Case Study on Quick Sort | p. 150 |
| Case Study on Industry Design (Low Pass Filter) | p. 151 |
| Related Work | p. 151 |
| Summary | p. 152 |
| Notes | p. 153 |
| BMC for Multi-Clock Systems | p. 155 |
| Introduction | p. 155 |
| Nested Clock Specifications | p. 155 |
| Verification Model for Multi-clock Systems | p. 156 |
| Simplification of Verification Model | p. 156 |
| Clock Specification on Latches | p. 157 |
| Efficient Modeling of Multi-Clock Systems | p. 158 |
| Reducing Unrolling in BMC | p. 160 |
| Reducing Loop-Checks in BMC | p. 161 |
| Dynamic Simplification in BMC | p. 162 |
| Customization of Clocked Specifications in BMC | p. 163 |
| Experiments | p. 166 |
| VGA/LCD Controller | p. 167 |
| Tri-mode Ethernet MAC Controller | p. 168 |
| Related Work | p. 169 |
| Summary | p. 170 |
| Notes | p. 171 |
| Proof Methods | p. 173 |
| Proof by Induction | p. 175 |
| Introduction | p. 175 |
| BMC Procedure for Proof by Induction | p. 176 |
| Inductive Invariants: Reachability Constraints | p. 177 |
| Proof of Induction with EMM | p. 179 |
| Experiments | p. 180 |
| Use of Reachability Invaraints | p. 180 |
| Case Study: Use of Induction proof with EMM | p. 181 |
| Summary | p. 182 |
| Notes | p. 183 |
| Unbounded Model Checking | p. 185 |
| Introduction | p. 185 |
| Motivation | p. 187 |
| Circuit Cofactoring Approach | p. 188 |
| Basic Idea | p. 188 |
| The Procedure | p. 189 |
| Comparing circuit cofactoring with cube-wise enumeration | p. 190 |
| Cofactor Representation | p. 191 |
| Enumeration using Hybrid SAT | p. 192 |
| Heuristics to Enlarge the Satisfying State Set | p. 193 |
| SAT-based UMC | p. 197 |
| SAT-based Existential Quantification using Circuit Cofactor | p. 198 |
| SAT-based UMC for F(p) | p. 198 |
| SAT-based UMC for G(q) | p. 199 |
| SAT-based UMC for F(p[hat]G(q)) | p. 202 |
| Experiments for Safety Properties | p. 203 |
| Industry Benchmarks | p. 203 |
| Public Verification Benchmarks | p. 206 |
| Experiments for Liveness Properties | p. 207 |
| Related Work | p. 209 |
| Summary | p. 211 |
| Notes | p. 212 |
| Abstraction/Refinement | p. 213 |
| Proof-Based Iterative Abstraction | p. 215 |
| Introduction | p. 215 |
| Proof-Based Abstraction (PBA): Overview | p. 218 |
| Latch-based Abstraction | p. 219 |
| Pruning in Latch Interface Abstraction | p. 222 |
| Environmental Constraints | p. 223 |
| Latch Interface Propagation Constraints | p. 224 |
| Abstract Models | p. 225 |
| Improving Abstraction using Lazy Constraints | p. 226 |
| Making Eager Constraints Lazy | p. 227 |
| Iterative Abstraction Framework | p. 228 |
| Inner Loop of the Framework | p. 228 |
| Handling Counterexamples | p. 229 |
| Lazy Constraints in Iterative Framework | p. 230 |
| Application of Proof-based Iterative Abstraction | p. 231 |
| EMM with Proof-based Abstraction | p. 232 |
| Experimental Results of Latch-based Abstraction | p. 233 |
| Results for Iterative Abstraction | p. 233 |
| Results for Verification of Abstract Models | p. 235 |
| Experimental Results using Lazy Constraints | p. 236 |
| Results for Use of Lazy Constraints | p. 236 |
| Proofs on Final Abstract Models | p. 239 |
| Case study: EMM with PBIA | p. 240 |
| Related Work | p. 242 |
| Summary | p. 243 |
| Notes | p. 243 |
| Verification Procedure | p. 245 |
| SAT-Based Verification Framework | p. 247 |
| Introduction | p. 247 |
| Verification Model and Properties | p. 248 |
| Verification Engines | p. 250 |
| Verification Engine Analysis | p. 254 |
| Verification Strategies: Case Studies | p. 256 |
| Summary | p. 261 |
| Notes | p. 261 |
| Synthesis for Verification | p. 263 |
| Introduction | p. 263 |
| Current Methodology | p. 265 |
| Synthesis for Verification Paradigm | p. 267 |
| High-level Verification Models | p. 269 |
| High-level Synthesis (HLS) | p. 269 |
| Extended Finite State Machine (EFSM) Model | p. 269 |
| Flow Graphs | p. 271 |
| "BMC-friendly" Modeling Issues | p. 272 |
| Synthesizing "BMC-friendly" Models | p. 273 |
| EFSM Learning | p. 274 |
| Extraction: Control State Reachability (CSR) | p. 274 |
| On-the-Fly Simplification | p. 275 |
| Unreachablility of Control States | p. 277 |
| EFSM Transformations | p. 277 |
| Property-based EFSM Reduction | p. 278 |
| Balancing Re-convergence | p. 278 |
| Balancing Re-convergence without Loops | p. 280 |
| Balancing Re-convergence with Loops | p. 282 |
| High-level BMC on EFSM | p. 285 |
| Expression Simplifier | p. 286 |
| Incremental Learning in High-level BMC | p. 287 |
| Experiments | p. 287 |
| Controlled Case Study | p. 287 |
| Experiments on Industry Software bc-1.06 | p. 289 |
| Experiments on Industry Embedded System Software | p. 292 |
| Experiments on System-level Model | p. 293 |
| Summary and Future work | p. 294 |
| Notes | p. 295 |
| References | p. 297 |
| Glossary | p. 309 |
| Index | p. 317 |
| About the Authors | p. 325 |
| Table of Contents provided by Ingram. All Rights Reserved. |
