Advanced formal verification

Advanced Formal Verification......Page 1
Contents......Page 6
Preface......Page 12
Acknowledgment......Page 13
Contributing Authors......Page 14
1. Formal Verification......Page 20
2. Challenges......Page 22
3. Contributions to this Book......Page 24
References......Page 25
1. Introduction......Page 28
2.1 Introduction......Page 30
2.2 Common Specification of Boolean Circuits......Page 32
2.3 Equivalence Checking as SAT......Page 38
2.4 Class M(p) and general resolution......Page 39
2.5 Computation of existentially implied functions......Page 40
2.6 Equivalence Checking in General Resolution......Page 41
2.7 Equivalence Checking of Circuits with Unknown CS......Page 47
2.8 A Procedure of Equivalence Checking for Circuits with a Known CS......Page 49
2.9 Experimental Results......Page 50
3.1 Introduction......Page 53
3.2 Stable Set of Points......Page 55
3.3 SSP as a reachable set of points......Page 58
3.4 Testing Satisfiability of CNF Formulas by SSP Construction......Page 59
3.5 Testing Satisfiability of Symmetric CNF Formulas by SSP Construction......Page 62
3.6 SSPs with Excluded Directions......Page 66
References......Page 69
1. Introduction......Page 72
2.1 SAT Solvers......Page 74
2.2 Binary Decision Diagrams......Page 75
2.3 Model Checking and Equivalence Checking......Page 79
3.1 Theoretical Considerations......Page 81
3.2 Experimental Benchmarking......Page 82
3.3 Working on Affinities: Variable Order......Page 85
4. Decision Diagrams as a Slave Engine in general SAT: Clause Compression by Means of ZBDDs......Page 88
5. Decision Diagram Preprocessing and Circuit-Based SAT......Page 89
5.1 BED Preprocessing......Page 90
5.2 Circuit-Based SAT......Page 91
5.3 Preprocessing by Approximate Reachability......Page 94
6. Using SAT in Symbolic Reachability Analysis......Page 95
7. Conclusions, Remarks and Future Works......Page 98
References......Page 100
EQUIVALENCE CHECKING OF ARITHMETIC CIRCUITS......Page 104
1. Introduction......Page 105
2. Verification Using Functional Properties......Page 108
3. Bit-Level Decision Diagrams......Page 112
4. Word-Level Decision Diagrams......Page 115
4.1 Pseudo-Boolean functions and decompositions......Page 116
4.2 *BMDs......Page 119
4.3 Equivalence Checking Using *BMDs......Page 121
4.4 Experiments with *BMD synthesis......Page 124
5. Arithmetic Bit-Level Verification......Page 132
5.1 Verification at the Arithmetic Bit Level......Page 135
5.2 Extracting the Half Adder Network......Page 139
5.4 Experimental Results......Page 142
6. Conclusion......Page 145
7. Future Perspectives......Page 146
References......Page 147
Introduction......Page 152
1.1 Tool Environment......Page 153
1.2 The gateprop Property Checker......Page 154
2.1 From Property to Satisfiability......Page 156
2.2 Preserving Structure during Problem Construction......Page 158
2.3 The Experimental Platform RtProp......Page 159
3.1 Symmetry in Property Checking Problems......Page 160
3.2 Finding Symmetrical Value Vectors......Page 163
3.3 Practical Results......Page 167
4. Automated Data Path Scaling to Speed Up Property Checking......Page 169
4.1 Bitvector Satisfiability Problems......Page 170
4.2 Formal Abstraction Techniques......Page 172
4.3 Speeding Up Hardware Verification by One-To-One Abstraction......Page 173
4.4 Data Path Scaling of Circuit Designs......Page 174
5. Property Checking Use Cases......Page 179
5.1 Application Example: Reverse Engineering......Page 182
5.2 Application Example: Complete Block-Level ASIC Verification......Page 185
5.3 Productivity Statistics......Page 188
6.1 Achievements......Page 189
References......Page 190
1. Introduction......Page 194
1.1 Specifying properties......Page 196
1.2 Observability and controllability......Page 198
1.3 Formal property checking framework......Page 199
2.1 Temporal logic......Page 204
2.2 Property Specification Language (PSL)......Page 206
3. Assertion libraries......Page 210
4. Assertion simulation......Page 211
5.1 Handling complexity......Page 213
5.2 Formal property checking role......Page 217
6.1 On-line validation......Page 218
6.2 Synthesizable assertions......Page 219
6.3 Routing scheme for assertion libraries......Page 221
6.4 Assertion processors......Page 222
7. PCI property specification example......Page 224
7.1 PCI overview......Page 225
7.3 PCI burst order encoding requirement......Page 226
7.4 PCI basic read transaction......Page 227
8. Summary......Page 229
References......Page 230
FORMAL VERIFICATION FOR NONLINEAR ANALOG SYSTEMS: APPROACHES TO MODEL AND EQUIVALENCE CHECKING......Page 232
2. System Description......Page 233
2.2 State Space Description......Page 235
3. Equivalence Checking......Page 238
3.1 Basic Concepts......Page 239
3.2 Equivalence Checking Algorithm......Page 240
3.3 Linear Transformation Theory......Page 244
3.4 Experimental Results......Page 249
4.1 Model Checking Language......Page 254
4.2 Analog Model Checking Algorithm......Page 257
4.3 Experimental Results......Page 266
6. Acknowledgement......Page 269
References......Page 270
Index......Page 274
End of the Book......Page 276