دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش:
نویسندگان: Rolf Drechsler
سری:
ISBN (شابک) : 1402025300, 1402077211
ناشر: Kluwer Academic Publishers
سال نشر: 2004
تعداد صفحات: 276
زبان: English
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود)
حجم فایل: 4 مگابایت
در صورت تبدیل فایل کتاب Advanced formal verification به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب تأیید رسمی رسمی نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
Advanced Formal Verification آخرین پیشرفتها در حوزه تأیید را از دیدگاه کاربر و توسعهدهنده نشان میدهد. کارشناسان برجسته جهان، روشهای اساسی ابزارهای راستیآزمایی امروزی را توصیف میکنند و سناریوهای مختلفی را از عملکرد صنعتی توصیف میکنند. در بخش اول کتاب به تکنیک های اصلی ابزارهای تأیید رسمی امروزی، مانند SAT و BDD پرداخته شده است. علاوه بر این، ضربکنندههای که به سختی شناخته شدهاند، مطالعه میشوند. بخش دوم بینشی در مورد ابزارهای حرفه ای و روش های اساسی، مانند بررسی اموال و تأیید مبتنی بر ادعا می دهد. در نهایت، اجزای آنالوگ باید در نظر گرفته شوند تا با سیستم کامل بر روی طرح های تراشه کنار بیایند. بیشتر بخوانید...
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. Read more...
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