Sat-based Scalable Formal Verification Solutions

by Ganai, Malay; Gupta, Aarti

• ISBN13: 9780387691664
• ISBN10: 0387691669
• Format: Hardcover
• Copyright: 2007-07-01
• Publisher: Springer-Verlag New York Inc

Summary

Functional verification has become an important aspect of the chip design process. Significant resources, both in industry and academia, are devoted to the design complexity and verification endeavors. SAT-Based Scalable Formal Verification Solutions discusses in detail several of the latest and interesting scalable SAT-based techniques including: Hybrid SAT Solver, Customized Bounded/Unbounded Model Checking, Distributed Model Checking, Proofs and Proof-based Abstraction Methods, Verification of Embedded Memory System & Multi-clock Systems, and Synthesis for Verification Paradigm. These techniques have been designed and implemented in a verification platform Verisol (formally called DiVer) and have been used successfully in industry. This book provides algorithmic details and engineering insights into devising scalable approaches for an effective realization. It also includes the authors' practical experiences and recommendations in verifying the large industry designs using VeriSol. The book is primarily written for researchers, scientists, and verification engineers who would like to gain an in-depth understanding of scalable SAT-based verification techniques. The book will also be of interest for CAD tool developers who would like to incorporate various SAT-based advanced techniques in their products.

Table of Contents

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.