Advanced formal verification

✍ Scribed by Drechsler R. (ed.)

• Publisher: Springer
• Year: 2004
• Tongue: English
• Leaves: 276
• 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

Cover......Page 1
Contents......Page 6
Preface......Page 12
Contributing Authors......Page 14
1 Formal Verification......Page 20
2 Challenges......Page 22
3 Contributions to this Book......Page 24
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
3.7 Conclusions......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.1 ZBDDs for Symbolic Davis-Putnam Resolution......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
6.0.1 BDDs at SAT leaves......Page 96
6.0.2 SAT-Based Symbolic Image and Pre-image......Page 97
7 Conclusions, Remarks and Future Works......Page 98
3 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
4 Application of Property Checking and Underlying Techniques......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
6.2 Challenges and Perspectives......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
6 Formal Verification for Nonlinear Analog Systems......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
Appendix: Mathematical Symbols......Page 270
F......Page 274
T......Page 275
Z......Page 276