Advanced Formal Verification

✍ Scribed by Rolf Drechsler

• Publisher: Springer
• Year: 2004
• Tongue: English
• Leaves: 277
• Edition: 1
• Category: Library

✦ Synopsis

Advanced Formal Verification shows the latest developments in the verification domain from the perspectives of the user and the developer. World leading experts describe the underlying methods of today's verification tools and describe various scenarios from industrial practice. In the first part of the book the core techniques of today's formal verification tools, such as SAT and BDDs are addressed. In addition, multipliers, which are known to be difficult, are studied. The second part gives insight in professional tools and the underlying methodology, such as property checking and assertion based verification. Finally, analog components have to be considered to cope with complete system on chip designs.

✦ Table of Contents

Team LiB......Page 1
Cover......Page 2
Contents......Page 7
Preface......Page 13
Contributing Authors......Page 15
1 Formal Verification......Page 21
2 Challenges......Page 23
3 Contributions to this Book......Page 25
1 Introduction......Page 29
2.1 Introduction......Page 31
2.2 Common Specification of Boolean Circuits......Page 33
2.3 Equivalence Checking as SAT......Page 39
2.4 Class M(p) and general resolution......Page 40
2.5 Computation of existentially implied functions......Page 41
2.6 Equivalence Checking in General Resolution......Page 42
2.7 Equivalence Checking of Circuits with Unknown CS......Page 48
2.8 A Procedure of Equivalence Checking for Circuits with a Known CS......Page 50
2.9 Experimental Results......Page 51
3.1 Introduction......Page 54
3.2 Stable Set of Points......Page 56
3.3 SSP as a reachable set of points......Page 59
3.4 Testing Satisfiability of CNF Formulas by SSP Construction......Page 60
3.5 Testing Satisfiability of Symmetric CNF Formulas by SSP Construction......Page 63
3.6 SSPs with Excluded Directions......Page 67
3.7 Conclusions......Page 70
1 Introduction......Page 73
2.1 SAT Solvers......Page 75
2.2 Binary Decision Diagrams......Page 76
2.3 Model Checking and Equivalence Checking......Page 80
3.1 Theoretical Considerations......Page 82
3.2 Experimental Benchmarking......Page 83
3.3 Working on Affinities: Variable Order......Page 86
4.1 ZBDDs for Symbolic Davis-Putnam Resolution......Page 89
5 Decision Diagram Preprocessing and Circuit-Based SAT......Page 90
5.1 BED Preprocessing......Page 91
5.2 Circuit-Based SAT......Page 92
5.3 Preprocessing by Approximate Reachability......Page 95
6 Using SAT in Symbolic Reachability Analysis......Page 96
6.0.1 BDDs at SAT leaves......Page 97
6.0.2 SAT-Based Symbolic Image and Pre-image......Page 98
7 Conclusions, Remarks and Future Works......Page 99
3 Equivalence Checking of Arithmetic Circuits......Page 105
1 Introduction......Page 106
2 Verification Using Functional Properties......Page 109
3 Bit-Level Decision Diagrams......Page 113
4 Word-Level Decision Diagrams......Page 116
4.1 Pseudo-Boolean functions and decompositions......Page 117
4.2 BMDs......Page 120
4.3 Equivalence Checking Using BMDs......Page 122
4.4 Experiments with *BMD synthesis......Page 125
5 Arithmetic Bit-Level Verification......Page 133
5.1 Verification at the Arithmetic Bit Level......Page 136
5.2 Extracting the Half Adder Network......Page 140
5.4 Experimental Results......Page 143
6 Conclusion......Page 146
7 Future Perspectives......Page 147
4 Application of Property Checking and Underlying Techniques......Page 153
1.1 Tool Environment......Page 154
1.2 The gateprop Property Checker......Page 155
2.1 From Property to Satisfiability......Page 157
2.2 Preserving Structure during Problem Construction......Page 159
2.3 The Experimental Platform RtProp......Page 160
3.1 Symmetry in Property Checking Problems......Page 161
3.2 Finding Symmetrical Value Vectors......Page 164
3.3 Practical Results......Page 168
4 Automated Data Path Scaling to Speed Up Property Checking......Page 170
4.1 Bitvector Satisfiability Problems......Page 171
4.2 Formal Abstraction Techniques......Page 173
4.3 Speeding Up Hardware Verification by One-To-One Abstraction......Page 174
4.4 Data Path Scaling of Circuit Designs......Page 175
5 Property Checking Use Cases......Page 180
5.1 Application Example: Reverse Engineering......Page 183
5.2 Application Example: Complete Block-Level ASIC Verification......Page 186
5.3 Productivity Statistics......Page 189
6.1 Achievements......Page 190
6.2 Challenges and Perspectives......Page 191
1 Introduction......Page 195
1.1 Specifying properties......Page 197
1.2 Observability and controllability......Page 199
1.3 Formal property checking framework......Page 200
2.1 Temporal logic......Page 205
2.2 Property Specification Language (PSL)......Page 207
3 Assertion libraries......Page 211
4 Assertion simulation......Page 212
5.1 Handling complexity......Page 214
5.2 Formal property checking role......Page 218
6.1 On-line validation......Page 219
6.2 Synthesizable assertions......Page 220
6.3 Routing scheme for assertion libraries......Page 222
6.4 Assertion processors......Page 223
7 PCI property specification example......Page 225
7.1 PCI overview......Page 226
7.3 PCI burst order encoding requirement......Page 227
7.4 PCI basic read transaction......Page 228
8 Summary......Page 230
6 Formal Verification for Nonlinear Analog Systems......Page 233
2 System Description......Page 234
2.2 State Space Description......Page 236
3 Equivalence Checking......Page 239
3.1 Basic Concepts......Page 240
3.2 Equivalence Checking Algorithm......Page 241
3.3 Linear Transformation Theory......Page 245
3.4 Experimental Results......Page 250
4.1 Model Checking Language......Page 255
4.2 Analog Model Checking Algorithm......Page 258
4.3 Experimental Results......Page 267
6 Acknowledgement......Page 270
Appendix: Mathematical Symbols......Page 271
F......Page 275
T......Page 276
Z......Page 277