Ganai / Gupta SAT-Based Scalable Formal Verification Solutions

1. Auflage 2007
ISBN: 978-0-387-69167-1
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 330 Seiten

Reihe: Integrated Circuits and Systems

This book provides an engineering insight into how to provide a scalable and robust verification solution with ever increasing design complexity and sizes. It describes SAT-based model checking approaches and gives engineering details on what makes model checking practical. The book brings together the various SAT-based scalable emerging technologies and techniques covered can be synergistically combined into a scalable solution.

Autoren/Hrsg.

Ganai, Malay

Gupta, Aarti

Inhaltsverzeichnis

1;Preface;8
2;Contents;12
3;List of Figures;20
4;List of Tables;28
5;1 DESIGN VERIFICATION CHALLENGES;31
5.1;1.1 Introduction;31
5.2;1.2 Simulation-based Verification;31
5.3;1.3 Formal Verification;32
5.3.1;1.3.1 Model Checking;33
5.4;1.4 Overview;35
5.5;1.5 Verification Tasks;36
5.6;1.6 Verification Challenges;38
5.6.1;1.6.1 Design Features;38
5.6.2;1.6.2 Verification Techniques;39
5.6.3;1.6.3 Verification Methodology;41
5.7;1.7 Organization of Book;43
6;2 BACKGROUND;47
6.1;2.1 Model Checking;47
6.1.1;2.1.1 Correctness Properties;48
6.1.2;2.1.2 Explicit Model Checking;49
6.1.3;2.1.3 Symbolic Model Checking;49
6.2;2.2 Notations;50
6.3;2.3 Binary Decision Diagrams;52
6.4;2.4 Boolean Satisfiability Problem;53
6.4.1;2.4.1 Decision Engine;55
6.4.2;2.4.2 Deduction Engine;56
6.4.3;2.4.3 Diagnosis Engine;58
6.4.4;2.4.4 Proof of Unsatisfiability;59
6.4.5;2.4.5 Further Improvements;60
6.5;2.5 SAT-based Bounded Model Checking (BMC);62
6.5.1;2.5.1 BMC formulation: Safety and Liveness Properties;63
6.5.2;2.5.2 Clocked LTL Specifications;66
6.6;2.6 SAT-based Unbounded Model Checking;67
6.7;2.7 SMT-based BMC;69
6.8;2.8 Notes;70
7;PART I: BASIC INFRASTRUCTURE;72
7.1;3 EFFICIENT BOOLEAN REPRESENTATION;73
7.1.1;3.1 Introduction;73
7.1.2;3.2 Brief Survey of Boolean Representations;75
7.1.2.1;3.2.1 Extended Boolean Decision Diagrams (XBDDs);75
7.1.2.2;3.2.2 Boolean Expression Diagrams (BEDs);75
7.1.2.3;3.2.3 AND/INVERTER Graph (AIG);76
7.1.3;3.3 Functional Hashing (Reduced AIG);79
7.1.3.1;3.3.1 Three-Input Case;80
7.1.3.2;3.3.2 Four-Input Case;82
7.1.3.3;3.3.3 Example;84
7.1.4;3.4 Experiments;87
7.1.5;3.5 Simplification using External Constraints;90
7.1.6;3.6 Sweeping Comparing Functional Hashing with BDD/ SAT;91
7.1.7;3.7 Summary;92
7.1.8;3.8 Notes;92
7.2;4 HYBRID DPLL-STYLE SAT SOLVER;93
7.2.1;4.1 Introduction;93
7.2.2;4.2 BCP on Circuit;95
7.2.3;4.3 Hybrid SAT Solver;98
7.2.3.1;4.3.1 Proof of Unsatisfiability;99
7.2.3.2;4.3.2 Comparison with Chaff;99
7.2.4;4.4 Applying Circuit-based Heuristics;101
7.2.4.1;4.4.1 Justification Frontier Heuristics;101
7.2.4.2;4.4.2 Implication Order;102
7.2.4.3;4.4.3 Gate Fanout Count;103
7.2.4.4;4.4.4 Learning XOR/MUX Gates;104
7.2.5;4.5 Verification Applications of Hybrid SAT Solver;105
7.2.6;4.6 Summary;105
7.2.7;4.7 Notes;106
8;PART II: FALSIFICATION;108
8.1;5 SAT-BASED BOUNDED MODEL CHECKING;109
8.1.1;5.1 Introduction;109
8.1.2;5.2 Dynamic Circuit Simplification;111
8.1.2.1;5.2.1 Notation;112
8.1.2.2;5.2.2 Procedure;113
8.1.2.3;5.2.3 Comparing Implicit with Explicit Unrolling;114
8.1.3;5.3 SAT-based Incremental Learning and Simplification;116
8.1.4;5.4 BDD-based Learning;120
8.1.4.1;5.4.1 Basic Idea;120
8.1.4.2;5.4.2 Procedure:;121
8.1.4.3;5.4.3 Seed Selection;122
8.1.4.4;5.4.4 Creation of BDDs;123
8.1.4.5;5.4.5 Generation of Learned Clauses;124
8.1.4.6;5.4.6 Integrating BDD Learning with a Hybrid SAT Solver;125
8.1.4.7;5.4.7 Adding Clauses Dynamically to a SAT Solver;125
8.1.4.8;5.4.8 Heuristics for Adding Learned Clauses;126
8.1.4.9;5.4.9 Application of BDD-based Learning;127
8.1.5;5.5 Customized Property Translation;128
8.1.5.1;5.5.1 Customized Translation for F(p);130
8.1.5.2;5.5.2 Customized Translation of G(q);132
8.1.5.3;5.5.3 Customized Translation of F(pG(q));133
8.1.6;5.6 Experiments;134
8.1.6.1;5.6.1 Comparative Study of Various Techniques;135
8.1.6.2;5.6.2 Effect of Customized Translation and Incremental Learning;138
8.1.6.3;5.6.3 Effect of BDD-based Learning on BMC;139
8.1.6.4;5.6.4 Static BDD Learning;139
8.1.6.5;5.6.5 Dynamic BDD Learning;140
8.1.7;5.7 Summary;142
8.1.8;5.8 Notes;142
8.2;6 DISTRIBUTED SAT-BASED BMC;143
8.2.1;6.1 Introduction;143
8.2.2;6.2 Distributed SAT-based BMC Procedure;144
8.2.3;6.3 Topology-cognizant Distributed-BCP;146
8.2.4;6.4 Distributed-SAT;148
8.2.4.1;6.4.1 Tasks of the Master;149
8.2.4.2;6.4.2 Tasks of a Client Ci;150
8.2.5;6.5 SAT-based Distributed-BMC;150
8.2.6;6.6 Optimizations;151
8.2.6.1;6.6.1 Memory Optimizations in Distributed-SAT;151
8.2.6.2;6.6.2 Tight Estimation of Communication Overhead;151
8.2.6.3;6.6.3 Performance Optimizations in Distributed-SAT;153
8.2.6.4;6.6.4 Performance Optimization in SAT-based Distributed-BMC;154
8.2.7;6.7 Experiments;154
8.2.8;6.8 Related Work;158
8.2.9;6.9 Summary;159
8.2.10;6.10 Notes;159
8.3;7 EFFICIENT MEMORY MODELING IN BMC;161
8.3.1;7.1 Introduction;161
8.3.2;7.2 Basic Idea;162
8.3.3;7.3 Memory Semantics;164
8.3.4;7.4 EMM Approach;165
8.3.4.1;7.4.1 Efficient Representation of Memory Modeling Constraints;166
8.3.4.2;7.4.2 Comparison with ITE Representation;169
8.3.4.3;7.4.3 Non-uniform Initialization of Memory;170
8.3.4.4;7.4.4 EMM for Multiple Memories, Read, and Write Ports;171
8.3.4.5;7.4.5 Arbitrary Initial Memory State;173
8.3.5;7.5 Experiments on a Single Read/Write Port Memory;174
8.3.6;7.6 Experiments on Multi-Port Memories;179
8.3.6.1;7.6.1 Case Study on Quick Sort;180
8.3.6.2;7.6.2 Case Study on Industry Design (Low Pass Filter);181
8.3.7;7.7 Related Work;181
8.3.8;7.8 Summary;182
8.3.9;7.9 Notes;183
8.4;8 BMC FOR MULTI-CLOCK SYSTEMS;185
8.4.1;8.1 Introduction;185
8.4.1.1;8.1.1 Nested Clock Specifications;185
8.4.1.2;8.1.2 Verification Model for Multi-clock Systems;186
8.4.1.3;8.1.3 Simplification of Verification Model;186
8.4.1.4;8.1.4 Clock Specification on Latches;187
8.4.2;8.2 Efficient Modeling of Multi-Clock Systems;188
8.4.3;8.3 Reducing Unrolling in BMC;190
8.4.4;8.4 Reducing Loop-Checks in BMC;191
8.4.5;8.5 Dynamic Simplification in BMC;192
8.4.6;8.6 Customization of Clocked Specifications in BMC;193
8.4.7;8.7 Experiments;196
8.4.7.1;8.7.1 VGA/LCD Controller;197
8.4.7.2;8.7.2 Tri-mode Ethernet MAC Controller;198
8.4.8;8.8 Related Work;199
8.4.9;8.9 Summary;200
8.4.10;8.10 Notes;201
9;PART III: PROOF METHODS;203
9.1;9 PROOF BY INDUCTION;205
9.1.1;9.1 Introduction;205
9.1.2;9.2 BMC Procedure for Proof by Induction ;206
9.1.3;9.3 Inductive Invariants:;207
9.1.4;9.4 Proof of Induction with EMM;209
9.1.5;9.5 Experiments;210
9.1.5.1;9.5.1 Use of Reachability Invaraints;210
9.1.5.2;9.5.2 Case Study: Use of Induction proof with EMM;211
9.1.6;9.6 Summary;212
9.1.7;9.7 Notes;213
9.2;10 UNBOUNDED MODEL CHECKING;215
9.2.1;10.1 Introduction;215
9.2.2;10.2 Motivation;217
9.2.3;10.3 Circuit Cofactoring Approach;218
9.2.4;10.4 Cofactor Representation;221
9.2.5;10.5 Enumeration using Hybrid SAT;222
9.2.6;10.6 SAT-based UMC;227
9.2.7;10.7 Experiments for Safety Properties;233
9.2.7.1;10.7.1 Industry Benchmarks;233
9.2.7.2;10.7.2 Public Verification Benchmarks;236
9.2.8;10.8 Experiments for Liveness Properties;237
9.2.9;10.9 Related Work;239
9.2.10;10.10 Summary;241
9.2.11;10.11 Notes;242
10;PART IV: ABSTRACTION/REFINEMENT;244
10.1;11 PROOF-BASED ITERATIVE ABSTRACTION;245
10.1.1;11.1 Introduction;245
10.1.2;11.2 Proof-Based Abstraction (PBA): Overview;248
10.1.3;11.3 Latch-based Abstraction;249
10.1.4;11.4 Pruning in Latch Interface Abstraction;252
10.1.4.1;11.4.1 Environmental Constraints;253
10.1.4.2;11.4.2 Latch Interface Propagation Constraints;254
10.1.5;11.5 Abstract Models;255
10.1.6;11.6 Improving Abstraction using Lazy Constraints;256
10.1.7;11.7 Iterative Abstraction Framework;258
10.1.7.1;11.7.1 Inner Loop of the Framework;258
10.1.7.2;11.7.2 Handling Counterexamples;259
10.1.7.3;11.7.3 Lazy Constraints in Iterative Framework;260
10.1.8;11.8 Application of Proof-based Iterative Abstraction;261
10.1.9;11.9 EMM with Proof-based Abstraction;262
10.1.10;11.10 Experimental Results of Latch-based Abstraction;263
10.1.10.1;11.10.1 Results for Iterative Abstraction;263
10.1.10.2;11.10.2 Results for Verification of Abstract Models;265
10.1.11;11.11 Experimental Results using Lazy Constraints;266
10.1.11.1;11.11.1 Results for Use of Lazy Constraints;266
10.1.11.2;11.11.2 Proofs on Final Abstract Models;269
10.1.12;11.12 Case study: EMM with PBIA;270
10.1.13;11.13 Related Work;272
10.1.14;11.14 Summary;273
10.1.15;11.15 Notes;273
11;PART V: VERIFICATION PROCEDURE;275
11.1;12 SAT-BASED VERIFICATION FRAMEWORK;277
11.1.1;12.1 Introduction;277
11.1.2;12.2 Verification Model and Properties;278
11.1.3;12.3 Verification Engines;280
11.1.4;12.4 Verification Engine Analysis;284
11.1.5;12.5 Verification Strategies: Case Studies;286
11.1.6;12.6 Summary;291
11.1.7;12.7 Notes;291
11.2;13 SYNTHESIS FOR VERIFICATION;293
11.2.1;13.1 Introduction;293
11.2.2;13.2 Current Methodology;295
11.2.3;13.3 Synthesis for Verification Paradigm;297
11.2.4;13.4 High-level Verification Models;299
11.2.4.1;13.4.1 High-level Synthesis (HLS);299
11.2.4.2;13.4.2 Extended Finite State Machine (EFSM) Model;299
11.2.4.3;13.4.3 Flow Graphs;301
11.2.5;13.5 “BMC-friendly” Modeling Issues;302
11.2.6;13.6 Synthesizing “BMC-friendly” Models;303
11.2.7;13.7 EFSM Learning;304
11.2.7.1;13.7.1 Extraction: Control State Reachability (CSR);304
11.2.7.2;13.7.2 On-the-Fly Simplification;305
11.2.7.3;13.7.3 Unreachablility of Control States;307
11.2.8;13.8 EFSM Transformations;307
11.2.8.1;13.8.1 Property-based EFSM Reduction;308
11.2.8.2;13.8.2 Balancing Re-convergence;308
11.2.8.3;13.8.3 Balancing Re-convergence without Loops;310
11.2.8.4;13.8.4 Balancing Re-convergence with Loops;312
11.2.8.5;Problem 13.3:;313
11.2.9;13.9 High-level BMC on EFSM;315
11.2.9.1;13.9.1 Expression Simplifier;316
11.2.9.2;13.9.2 Incremental Learning in High-level BMC;317
11.2.10;13.10 Experiments;317
11.2.10.1;13.10.1 Controlled Case Study;317
11.2.10.2;13.10.2 Experiments on Industry Software;319
11.2.10.3;13.10.3 Experiments on Industry Embedded System Software;322
11.2.10.4;13.10.4 Experiments on System-level Model;323
11.2.11;13.11 Summary and Future work;324
11.2.12;13.12 Notes;325
12;References;327
13;Glossary;339
14;Index;347
15;About the Authors;355

Leseproben

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).