SAT-Based Scalable Formal Verification Solutions (eBook)

Preface 8
Contents 12
List of Figures 20
List of Tables 28
1 DESIGN VERIFICATION CHALLENGES 31
1.1 Introduction 31
1.2 Simulation-based Verification 31
1.3 Formal Verification 32
1.3.1 Model Checking 33
1.4 Overview 35
1.5 Verification Tasks 36
1.6 Verification Challenges 38
1.6.1 Design Features 38
1.6.2 Verification Techniques 39
1.6.3 Verification Methodology 41
1.7 Organization of Book 43
2 BACKGROUND 47
2.1 Model Checking 47
2.1.1 Correctness Properties 48
2.1.2 Explicit Model Checking 49
2.1.3 Symbolic Model Checking 49
2.2 Notations 50
2.3 Binary Decision Diagrams 52
2.4 Boolean Satisfiability Problem 53
2.4.1 Decision Engine 55
2.4.2 Deduction Engine 56
2.4.3 Diagnosis Engine 58
2.4.4 Proof of Unsatisfiability 59
2.4.5 Further Improvements 60
2.5 SAT-based Bounded Model Checking (BMC) 62
2.5.1 BMC formulation: Safety and Liveness Properties 63
2.5.2 Clocked LTL Specifications 66
2.6 SAT-based Unbounded Model Checking 67
2.7 SMT-based BMC 69
2.8 Notes 70
PART I: BASIC INFRASTRUCTURE 72
3 EFFICIENT BOOLEAN REPRESENTATION 73
3.1 Introduction 73
3.2 Brief Survey of Boolean Representations 75
3.2.1 Extended Boolean Decision Diagrams (XBDDs) 75
3.2.2 Boolean Expression Diagrams (BEDs) 75
3.2.3 AND/INVERTER Graph (AIG) 76
3.3 Functional Hashing (Reduced AIG) 79
3.3.1 Three-Input Case 80
3.3.2 Four-Input Case 82
3.3.3 Example 84
3.4 Experiments 87
3.5 Simplification using External Constraints 90
3.6 Sweeping Comparing Functional Hashing with BDD/ SAT 91
3.7 Summary 92
3.8 Notes 92
4 HYBRID DPLL-STYLE SAT SOLVER 93
4.1 Introduction 93
4.2 BCP on Circuit 95
4.3 Hybrid SAT Solver 98
4.3.1 Proof of Unsatisfiability 99
4.3.2 Comparison with Chaff 99
4.4 Applying Circuit-based Heuristics 101
4.4.1 Justification Frontier Heuristics 101
4.4.2 Implication Order 102
4.4.3 Gate Fanout Count 103
4.4.4 Learning XOR/MUX Gates 104
4.5 Verification Applications of Hybrid SAT Solver 105
4.6 Summary 105
4.7 Notes 106
PART II: FALSIFICATION 108
5 SAT-BASED BOUNDED MODEL CHECKING 109
5.1 Introduction 109
5.2 Dynamic Circuit Simplification 111
5.2.1 Notation 112
5.2.2 Procedure 113
5.2.3 Comparing Implicit with Explicit Unrolling 114
5.3 SAT-based Incremental Learning and Simplification 116
5.4 BDD-based Learning 120
5.4.1 Basic Idea 120
5.4.2 Procedure: 121
5.4.3 Seed Selection 122
5.4.4 Creation of BDDs 123
5.4.5 Generation of Learned Clauses 124
5.4.6 Integrating BDD Learning with a Hybrid SAT Solver 125
5.4.7 Adding Clauses Dynamically to a SAT Solver 125
5.4.8 Heuristics for Adding Learned Clauses 126
5.4.9 Application of BDD-based Learning 127
5.5 Customized Property Translation 128
5.5.1 Customized Translation for F(p) 130
5.5.2 Customized Translation of G(q) 132
5.5.3 Customized Translation of F(pG(q)) 133
5.6 Experiments 134
5.6.1 Comparative Study of Various Techniques 135
5.6.2 Effect of Customized Translation and Incremental Learning 138
5.6.3 Effect of BDD-based Learning on BMC 139
5.6.4 Static BDD Learning 139
5.6.5 Dynamic BDD Learning 140
5.7 Summary 142
5.8 Notes 142
6 DISTRIBUTED SAT-BASED BMC 143
6.1 Introduction 143
6.2 Distributed SAT-based BMC Procedure 144
6.3 Topology-cognizant Distributed-BCP 146
6.4 Distributed-SAT 148
6.4.1 Tasks of the Master 149
6.4.2 Tasks of a Client Ci 150
6.5 SAT-based Distributed-BMC 150
6.6 Optimizations 151
6.6.1 Memory Optimizations in Distributed-SAT 151
6.6.2 Tight Estimation of Communication Overhead 151
6.6.3 Performance Optimizations in Distributed-SAT 153
6.6.4 Performance Optimization in SAT-based Distributed-BMC 154
6.7 Experiments 154
6.8 Related Work 158
6.9 Summary 159
6.10 Notes 159
7 EFFICIENT MEMORY MODELING IN BMC 161
7.1 Introduction 161
7.2 Basic Idea 162
7.3 Memory Semantics 164
7.4 EMM Approach 165
7.4.1 Efficient Representation of Memory Modeling Constraints 166
7.4.2 Comparison with ITE Representation 169
7.4.3 Non-uniform Initialization of Memory 170
7.4.4 EMM for Multiple Memories, Read, and Write Ports 171
7.4.5 Arbitrary Initial Memory State 173
7.5 Experiments on a Single Read/Write Port Memory 174
7.6 Experiments on Multi-Port Memories 179
7.6.1 Case Study on Quick Sort 180
7.6.2 Case Study on Industry Design (Low Pass Filter) 181
7.7 Related Work 181
7.8 Summary 182
7.9 Notes 183
8 BMC FOR MULTI-CLOCK SYSTEMS 185
8.1 Introduction 185
8.1.1 Nested Clock Specifications 185
8.1.2 Verification Model for Multi-clock Systems 186
8.1.3 Simplification of Verification Model 186
8.1.4 Clock Specification on Latches 187
8.2 Efficient Modeling of Multi-Clock Systems 188
8.3 Reducing Unrolling in BMC 190
8.4 Reducing Loop-Checks in BMC 191
8.5 Dynamic Simplification in BMC 192
8.6 Customization of Clocked Specifications in BMC 193
8.7 Experiments 196
8.7.1 VGA/LCD Controller 197
8.7.2 Tri-mode Ethernet MAC Controller 198
8.8 Related Work 199
8.9 Summary 200
8.10 Notes 201
PART III: PROOF METHODS 203
9 PROOF BY INDUCTION 205
9.1 Introduction 205
9.2 BMC Procedure for Proof by Induction 206
9.3 Inductive Invariants: 207
9.4 Proof of Induction with EMM 209
9.5 Experiments 210
9.5.1 Use of Reachability Invaraints 210
9.5.2 Case Study: Use of Induction proof with EMM 211
9.6 Summary 212
9.7 Notes 213
10 UNBOUNDED MODEL CHECKING 215
10.1 Introduction 215
10.2 Motivation 217
10.3 Circuit Cofactoring Approach 218
10.4 Cofactor Representation 221
10.5 Enumeration using Hybrid SAT 222
10.6 SAT-based UMC 227
10.7 Experiments for Safety Properties 233
10.7.1 Industry Benchmarks 233
10.7.2 Public Verification Benchmarks 236
10.8 Experiments for Liveness Properties 237
10.9 Related Work 239
10.10 Summary 241
10.11 Notes 242
PART IV: ABSTRACTION/REFINEMENT 244
11 PROOF-BASED ITERATIVE ABSTRACTION 245
11.1 Introduction 245
11.2 Proof-Based Abstraction (PBA): Overview 248
11.3 Latch-based Abstraction 249
11.4 Pruning in Latch Interface Abstraction 252
11.4.1 Environmental Constraints 253
11.4.2 Latch Interface Propagation Constraints 254
11.5 Abstract Models 255
11.6 Improving Abstraction using Lazy Constraints 256
11.7 Iterative Abstraction Framework 258
11.7.1 Inner Loop of the Framework 258
11.7.2 Handling Counterexamples 259
11.7.3 Lazy Constraints in Iterative Framework 260
11.8 Application of Proof-based Iterative Abstraction 261
11.9 EMM with Proof-based Abstraction 262
11.10 Experimental Results of Latch-based Abstraction 263
11.10.1 Results for Iterative Abstraction 263
11.10.2 Results for Verification of Abstract Models 265
11.11 Experimental Results using Lazy Constraints 266
11.11.1 Results for Use of Lazy Constraints 266
11.11.2 Proofs on Final Abstract Models 269
11.12 Case study: EMM with PBIA 270
11.13 Related Work 272
11.14 Summary 273
11.15 Notes 273
PART V: VERIFICATION PROCEDURE 275
12 SAT-BASED VERIFICATION FRAMEWORK 277
12.1 Introduction 277
12.2 Verification Model and Properties 278
12.3 Verification Engines 280
12.4 Verification Engine Analysis 284
12.5 Verification Strategies: Case Studies 286
12.6 Summary 291
12.7 Notes 291
13 SYNTHESIS FOR VERIFICATION 293
13.1 Introduction 293
13.2 Current Methodology 295
13.3 Synthesis for Verification Paradigm 297
13.4 High-level Verification Models 299
13.4.1 High-level Synthesis (HLS) 299
13.4.2 Extended Finite State Machine (EFSM) Model 299
13.4.3 Flow Graphs 301
13.5 “BMC-friendly” Modeling Issues 302
13.6 Synthesizing “BMC-friendly” Models 303
13.7 EFSM Learning 304
13.7.1 Extraction: Control State Reachability (CSR) 304
13.7.2 On-the-Fly Simplification 305
13.7.3 Unreachablility of Control States 307
13.8 EFSM Transformations 307
13.8.1 Property-based EFSM Reduction 308
13.8.2 Balancing Re-convergence 308
13.8.3 Balancing Re-convergence without Loops 310
13.8.4 Balancing Re-convergence with Loops 312
Problem 13.3: 313
13.9 High-level BMC on EFSM 315
13.9.1 Expression Simplifier 316
13.9.2 Incremental Learning in High-level BMC 317
13.10 Experiments 317
13.10.1 Controlled Case Study 317
13.10.2 Experiments on Industry Software 319
13.10.3 Experiments on Industry Embedded System Software 322
13.10.4 Experiments on System-level Model 323
13.11 Summary and Future work 324
13.12 Notes 325
References 327
Glossary 339
Index 347
About the Authors 355

5 SAT-BASED BOUNDED MODEL CHECKING (p. 79-80)

5.1 Introduction

Bounded Model Checking (BMC) has been gaining ground as a falsification engine, mainly due to its improved scalability compared to other formal techniques. In BMC, the focus is on finding counterexamples (bugs) of a bounded length k. For a given design and correctness property, the problem is translated effectively to a propositional formula such that the formula is true if and only if a counterexample of length k exists [66, 67]. Such a translation basically involves unrolling the circuit of the transition relation for the required number of time frames as illustrated in Figure 5.1 (with k=d). Essentially, d copies of circuit are made and then clauses are built at each time frame for the unrolled circuit and the property to be reasoning is needed to ensure completeness when no counterexample can be found up to a certain bound [66, 67]. However, with increasing depth the problem size, comprising the unrolled circuit and translated property, grows linearly [111] with the size of the model, thereby the making the Boolean reasoning increasingly difficult for large bounds, in general. The standard translation for these properties is monolithic, i.e., the entire propositional formula is generated for a given k and then the formula is checked for satisfiability using a standard SAT solver. Such a monolithic translation provides little scope for an incremental formulation within a k-instance BMC problem. Therefore, the past efforts [153, 154] on incremental learning for BMC have been limited to sharing of constraints across k-instances only.

Outline

In this chapter, we discuss several enhancements proposed in the last few years to make the standard BMC procedure [66, 67] scale with large industry designs. The first key improvement that we discuss is dynamic circuit simplification [45] in Section 5.2. This is performed on the iterative array model of the unrolled transition relation, where an on-the-fly circuit reduction algorithm, discussed in Chapter 3, is applied not only within a single time frame but also across time frames to reduce the associated Boolean formula.

The second key enhancement we discuss is SAT-based incremental learning in Section 5.3. This is used to improve the overall verification time by re-using the SAT results from the previous runs. Next, we discuss a lightweight and goal-directed effective BDD-based learning scheme in Section 5.4, where learned clauses generated by BDDbased analysis are added to the SAT solver on-the-fly, to supplement its other learning mechanisms. We also discuss several heuristics for guiding the SAT search process to improve the performance of the BMC engine.

Based on the above simplification and learning techniques, we discuss the use of customized property translations, in Section 5.5, for commonly occurring LTL formulas such as safety and liveness, with novel features that utilize partitioning, learning, and incremental formulation [46]. Such customized translations allow not only incremental learning across kinstances, but also within k-instances of BMC problems and thereby, greatly improve overall performance. Moreover, in comparison to the standard translation, customized translations provide additional opportunities for deriving completeness bounds for nested properties (this is discussed in more detail in Chapter 10).