SAT-Based Scalable Formal Verification Solutions Book

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