Advanced Formal Verification

Drechsler R. (ed.)1402025300

Modern circuits may contain up to several hundred million transistors. In the meantime it has been observed that verification becomes the major bottleneck in design flows, i.e. up to 80% of the overall design costs are due to verification. This is one of the reasons why several methods have been proposed as alternatives to classical simulation. Simulation alone cannot guarantee sufficient coverage of the design resulting in bugs that may remain undetected.As alternatives formal verification techniques have been proposed. Instead of simulating a design the correctness is proven by formal techniques. There are different areas where these approaches can be used: equivalence checking, property checking or symbolic simulation. These methods have been successfully applied in many industrial projects and have become the state-of-the-art technique in several fields. However, the deployment of the existing tools in real-world projects also showed the weaknesses and problems of formal verification techniques. This gave motivating impulses for tool developers and researchers.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 assertionbased verification. Finally, analog components have to be considered to cope with complete system on chip designs.In this book the state-of-the-art in many important fields of formal verification are described. Besides the description of the most recent research results, open problems and challenging research areas are addressed. Because of this, the book is intended for CAD developers and researchers in the verification domain, where formal techniques become a core technology to successful circuit and system design. Furthermore, the book is an excellent reference for users of verification tools in order to acquire a better understanding of the internal principles and subsequently drive the tools to the highest performance. In this context the book is dedicated to those in industry and academia to stay informed about the most recent developments in the field of formal verification.

---

Table of contents :
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