SAT-based scalable formal verification solutions / Malay Ganai, Aarti Gupta.

Format:

Book

Author/Creator:

Ganai, Malay.

Contributor:

Gupta, Aarti.

Series:

Series on integrated circuits and systems

Language:

English

Subjects (All):

Integrated circuits--Verification.

Integrated circuits.

Physical Description:

xxix, 326 pages : illustrations ; 25 cm.

Place of Publication:

New York : Springer, 2007.

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.

Contents:

1 Design Verification Challenges 1

1.2 Simulation-based Verification 1

1.3 Formal Verification 2

1.3.1 Model Checking 3

1.5 Verification Tasks 6

1.6 Verification Challenges 8

1.6.1 Design Features 8

1.6.2 Verification Techniques 9

1.6.3 Verification Methodology 11

2.1 Model Checking 17

2.1.1 Correctness Properties 18

2.1.2 Explicit Model Checking 19

2.1.3 Symbolic Model Checking 19

2.3 Binary Decision Diagrams 22

2.4 Boolean Satisfiability Problem 23

2.4.1 Decision Engine 25

2.4.2 Deduction Engine 26

2.4.3 Diagnosis Engine 28

2.4.4 Proof of Unsatisfiability 29

2.4.5 Further Improvements 30

2.5 SAT-based Bounded Model Checking (BMC) 32

2.5.1 BMC formulation: Safety and Liveness Properties 33

2.5.2 Clocked LTL Specifications 36

2.6 SAT-based Unbounded Model Checking 37

2.7 SMT-based BMC 39

Part I Basic Infrastructure 41

3 Efficient Boolean Representation 43

3.2 Brief Survey of Boolean Representations 45

3.2.1 Extended Boolean Decision Diagrams (XBDDs) 45

3.2.2 Boolean Expression Diagrams (BEDs) 45

3.2.3 AND/INVERTER Graph (AIG) 46

3.3 Functional Hashing (Reduced AIG) 49

3.3.1 Three-Input Case 50

3.3.2 Four-Input Case 52

3.4 Experiments 57

3.5 Simplification using External Constraints 60

3.6 Comparing Functional Hashing with BDD/SAT Sweeping 61

4 Hybrid DPLL-Style SAT Solver 63

4.2 BCP on Circuit 65

4.2.1 Comparing CNF- and Circuit-based BCP Algorithms 67

4.3 Hybrid SAT Solver 68

4.3.1 Proof of Unsatisfiability 69

4.3.2 Comparison with Chaff 69

4.4 Applying Circuit-based Heuristics 71

4.4.1 Justification Frontier Heuristics 71

4.4.2 Implication Order 72

4.4.3 Gate Fanout Count 73

4.4.4 Learning XOR/MUX Gates 74

4.5 Verification Applications of Hybrid SAT Solver 75

Part II Falsification 77

5 SAT-Based Bounded Model Checking 79

5.2 Dynamic Circuit Simplification 81

5.2.2 Procedure Unroll 83

5.2.3 Comparing Implicit with Explicit Unrolling 84

5.3 SAT-based Incremental Learning and Simplification 86

5.4 BDD-based Learning 90

5.4.1 Basic Idea 90

5.4.2 Procedure: BDD_learning_engine 91

5.4.3 Seed Selection 92

5.4.4 Creation of BDDs 93

5.4.5 Generation of Learned Clauses 94

5.4.6 Integrating BDD Learning with a Hybrid SAT Solver 95

5.4.7 Adding Clauses Dynamically to a SAT Solver 95

5.4.8 Heuristics for Adding Learned Clauses 96

5.4.9 Application of BDD-based Learning 97

5.5 Customized Property Translation 98

5.5.1 Customized Translation for F(p) 100

5.5.2 Customized Translation of G(q) 102

5.5.3 Customized Translation of F(p[hat]G(q)) 103

5.6 Experiments 104

5.6.1 Comparative Study of Various Techniques 105

5.6.2 Effect of Customized Translation and Incremental Learning 108

5.6.3 Effect of BDD-based Learning on BMC 109

5.6.4 Static BDD Learning 109

5.6.5 Dynamic BDD Learning 110

6 Distributed SAT-Based BMC 113

6.2 Distributed SAT-based BMC Procedure 114

6.3 Topology-cognizant Distributed-BCP 116

6.3.1 Causal-effect Order 117

6.4 Distributed-SAT 118

6.4.1 Tasks of the Master 119

6.4.2 Tasks of a Client C[subscript i] 120

6.5 SAT-based Distributed-BMC 120

6.6 Optimizations 121

6.6.1 Memory Optimizations in Distributed-SAT 121

6.6.2 Tight Estimation of Communication Overhead 121

6.6.3 Performance Optimizations in Distributed-SAT 123

6.6.4 Performance Optimization in SAT-based Distributed-BMC 124

6.7 Experiments 124

7 Efficient Memory Modeling in BMC 131

7.2 Basic Idea 132

7.3 Memory Semantics 134

7.4 EMM Approach 135

7.4.1 Efficient Representation of Memory Modeling Constraints 136

7.4.2 Comparison with ITE Representation 139

7.4.3 Non-uniform Initialization of Memory 140

7.4.4 EMM for Multiple Memories, Read, and Write Ports 141

7.4.5 Arbitrary Initial Memory State 143

7.5 Experiments on a Single Read/Write Port Memory 144

7.6 Experiments on Multi-Port Memories 149

7.6.1 Case Study on Quick Sort 150

7.6.2 Case Study on Industry Design (Low Pass Filter) 151

8 BMC for Multi-Clock Systems 155

8.1.1 Nested Clock Specifications 155

8.1.2 Verification Model for Multi-clock Systems 156

8.1.3 Simplification of Verification Model 156

8.1.4 Clock Specification on Latches 157

8.2 Efficient Modeling of Multi-Clock Systems 158

8.3 Reducing Unrolling in BMC 160

8.4 Reducing Loop-Checks in BMC 161

8.5 Dynamic Simplification in BMC 162

8.6 Customization of Clocked Specifications in BMC 163

8.7 Experiments 166

8.7.1 VGA/LCD Controller 167

8.7.2 Tri-mode Ethernet MAC Controller 168

Part III Proof Methods 173

9 Proof by Induction 175

9.2 BMC Procedure for Proof by Induction 176

9.3 Inductive Invariants: Reachability Constraints 177

9.4 Proof of Induction with EMM 179

9.5 Experiments 180

9.5.1 Use of Reachability Invaraints 180

9.5.2 Case Study: Use of Induction proof with EMM 181

10 Unbounded Model Checking 185

10.2 Motivation 187

10.3 Circuit Cofactoring Approach 188

10.3.1 Basic Idea 188

10.3.2 The Procedure 189

10.3.3 Comparing circuit cofactoring with cube-wise enumeration 190

10.4 Cofactor Representation 191

10.5 Enumeration using Hybrid SAT 192

10.5.1 Heuristics to Enlarge the Satisfying State Set 193

10.6 SAT-based UMC 197

10.6.1 SAT-based Existential Quantification using Circuit Cofactor 198

10.6.2 SAT-based UMC for F(p) 198

10.6.3 SAT-based UMC for G(q) 199

10.6.4 SAT-based UMC for F(p[hat]G(q)) 202

10.7 Experiments for Safety Properties 203

10.7.1 Industry Benchmarks 203

10.7.2 Public Verification Benchmarks 206

10.8 Experiments for Liveness Properties 207

Part IV Abstraction/Refinement 213

11 Proof-Based Iterative Abstraction 215

11.2 Proof-Based Abstraction (PBA): Overview 218

11.3 Latch-based Abstraction 219

11.4 Pruning in Latch Interface Abstraction 222

11.4.1 Environmental Constraints 223

11.4.2 Latch Interface Propagation Constraints 224

11.5 Abstract Models 225

11.6 Improving Abstraction using Lazy Constraints 226

11.6.1 Making Eager Constraints Lazy 227

11.7 Iterative Abstraction Framework 228

11.7.1 Inner Loop of the Framework 228

11.7.2 Handling Counterexamples 229

11.7.3 Lazy Constraints in Iterative Framework 230

11.8 Application of Proof-based Iterative Abstraction 231

11.9 EMM with Proof-based Abstraction 232

11.10 Experimental Results of Latch-based Abstraction 233

11.10.1 Results for Iterative Abstraction 233

11.10.2 Results for Verification of Abstract Models 235

11.11 Experimental Results using Lazy Constraints 236

11.11.1 Results for Use of Lazy Constraints 236

11.11.2 Proofs on Final Abstract Models 239

11.12 Case study: EMM with PBIA 240

Part V Verification Procedure 245

12 SAT-Based Verification Framework 247

12.2 Verification Model and Properties 248

12.3 Verification Engines 250

12.4 Verification Engine Analysis 254

12.5 Verification Strategies: Case Studies 256

13 Synthesis for Verification 263

13.2 Current Methodology 265

13.3 Synthesis for Verification Paradigm 267

13.4 High-level Verification Models 269

13.4.1 High-level Synthesis (HLS) 269

13.4.2 Extended Finite State Machine (EFSM) Model 269

13.4.3 Flow Graphs 271

13.5 "BMC-friendly" Modeling Issues 272

13.6 Synthesizing "BMC-friendly" Models 273

13.7 EFSM Learning 274

13.7.1 Extraction: Control State Reachability (CSR) 274

13.7.2 On-the-Fly Simplification 275

13.7.3 Unreachablility of Control States 277

13.8 EFSM Transformations 277

13.8.1 Property-based EFSM Reduction 278

13.8.2 Balancing Re-convergence 278

13.8.3 Balancing Re-convergence without Loops 280

13.8.4 Balancing Re-convergence with Loops 282

13.9 High-level BMC on EFSM 285

13.9.1 Expression

Simplifier 286

13.9.2 Incremental Learning in High-level BMC 287

13.10 Experiments 287

13.10.1 Controlled Case Study 287

13.10.2 Experiments on Industry Software bc-1.06 289

13.10.3 Experiments on Industry Embedded System Software 292

13.10.4 Experiments on System-level Model 293

13.11 Summary and Future work 294.

Notes:

Includes bibliographical references and index.

ISBN:

9780387691664

0387691669

OCLC:

124025385