دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
دانلود کتاب Principles of Verifiable RTL Design: A functional coding style supporting verification processes in Verilog
دانلود کتاب اصول طراحی قابل تایید RTL: یک سبک کدگذاری کاربردی که از فرآیند تأیید در Verilog پشتیبانی می کند
مشخصات کتاب
Principles of Verifiable RTL Design: A functional coding style supporting verification processes in Verilog
ویرایش: 2
نویسندگان: Lionel Bening. Harry Foster (auth.)
سری:
ISBN (شابک) : 9780792373681, 9780306476310
ناشر: Springer US
سال نشر: 2002
تعداد صفحات: 296
زبان: English
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود)
حجم فایل: 5 مگابایت
قیمت کتاب (تومان) : 38,000
کلمات کلیدی مربوط به کتاب اصول طراحی قابل تایید RTL: یک سبک کدگذاری کاربردی که از فرآیند تأیید در Verilog پشتیبانی می کند: مدارها و سیستم ها، سخت افزار کامپیوتر، مهندسی به کمک کامپیوتر (CAD، CAE) و طراحی، مهندسی الکترونیک و کامپیوتر
در صورت تبدیل فایل کتاب Principles of Verifiable RTL Design: A functional coding style supporting verification processes in Verilog به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب اصول طراحی قابل تایید RTL: یک سبک کدگذاری کاربردی که از فرآیند تأیید در Verilog پشتیبانی می کند نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
توضیحاتی در مورد کتاب اصول طراحی قابل تایید RTL: یک سبک کدگذاری کاربردی که از فرآیند تأیید در Verilog پشتیبانی می کند
طراحان سیستم، دانشمندان کامپیوتر و مهندسان به طور مداوم نمادهایی را برای مدل‌سازی، مشخص‌سازی، شبیه‌سازی، مستندسازی، برقراری ارتباط، آموزش، تأیید و کنترل طرح‌های سیستم‌های دیجیتال اختراع و استفاده کرده‌اند. در ابتدا این طرح ها از طریق جزئیات الکترونیکی و ساختی ارائه می شدند. F- با افشاگری C. E. Shannon در سال 1948، نمودارهای منطقی و معادلات بولی برای نشان دادن سیستم های دیجیتال در یک فاکتور استفاده شد که در عین اینکه رفتار منطقی را آشکار می کرد، تأکید بر جزئیات الکترونیکی و ساختگی نداشت. تعداد کمی از مدارها برای حذف انتزاع این نمایش‌ها در مواقعی که انجام این کار مطلوب بود، در دسترس قرار گرفت. با افزایش پیچیدگی سیستم، نمودارهای بلوکی، نمودارهای زمان بندی، نمودارهای توالی و سایر نمادهای گرافیکی و نمادین در خلاصه کردن ویژگی های کلی یک سیستم و توصیف نحوه عملکرد آن مفید بودند. علاوه بر این، افزودن این اسناد با توضیحات شفاهی طولانی به زبان طبیعی، همیشه ضروری یا مناسب به نظر می رسید. در حالی که هر نماد یک ابزار کاملاً معتبر برای بیان یک طرح بود و هنوز هم هست، فقدان استانداردسازی، مختصر بودن و تعاریف نادرست در ارتباطات و درک بین گروه‌هایی از افراد که از نمادهای مختلف استفاده می‌کردند تداخل داشت. این مشکل در اوایل تشخیص داده شد و زبان های رسمی در دهه 1950 شروع به تکامل کردند، زمانی که I. S. Reed کشف کرد که معادلات ورودی فلیپ فلاپ معادل معادله انتقال ثبات و نماد xvi tor مانند هستند. با گسترش این مفاهیم، رید مفهومی را ایجاد کرد که به عنوان زبان انتقال ثبت (RTL) شناخته شد.
توضیحاتی درمورد کتاب به خارجی
System designers, computer scientists and engineers have c- tinuously invented and employed notations for modeling, speci- ing, simulating, documenting, communicating, teaching, verifying and controlling the designs of digital systems. Initially these s- tems were represented via electronic and fabrication details. F- lowing C. E. Shannon’s revelation of 1948, logic diagrams and Boolean equations were used to represent digital systems in a fa- ion that de-emphasized electronic and fabrication detail while revealing logical behavior. A small number of circuits were made available to remove the abstraction of these representations when it was desirable to do so. As system complexity grew, block diagrams, timing charts, sequence charts, and other graphic and symbolic notations were found to be useful in summarizing the gross features of a system and describing how it operated. In addition, it always seemed necessary or appropriate to augment these documents with lengthy verbal descriptions in a natural language. While each notation was, and still is, a perfectly valid means of expressing a design, lack of standardization, conciseness, and f- mal definitions interfered with communication and the understa- ing between groups of people using different notations. This problem was recognized early and formal languages began to evolve in the 1950s when I. S. Reed discovered that flip-flop input equations were equivalent to a register transfer equation, and that xvi tor-like notation. Expanding these concepts Reed developed a no- tion that became known as a Register Transfer Language (RTL).
فهرست مطالب
Principles of Verifiable RTL Design (2nd Ed.)......Page 1
Copyright......Page 5
Table of Contents......Page 8
Foreword......Page 16
Preface......Page 20
Ch1 Introduction......Page 26
1.1.1 What is it?......Page 27
1.1.2 Verifiable RTL......Page 28
1.2 Assumptions......Page 29
1.3 Organization of this Book......Page 30
Ch2 Verification Process......Page 34
2.1 Specification Design Decomposition......Page 35
Fundamental Verification Principle......Page 36
2.1.4 Synthesis & Physical Design......Page 38
2.2 Functional Test Strategies......Page 39
2.2.1 Deterministic or Directed Test......Page 40
2.2.2 Random Test......Page 41
2.2.3 Transaction Analyzer Verification......Page 43
2.2.4 Chip Initialization Verification......Page 44
2.3 Transformation Test Strategies......Page 45
2.4 Summary......Page 46
Ch3 Coverage, Events & Assertions......Page 48
3.1 Coverage......Page 49
3.1.2 Programming Code Metrics......Page 50
3.1.5 Fault Coverage Metrics......Page 52
3.2 Event Monitors & Assertion Checkers......Page 53
3.2.1 Events......Page 54
3.2.2 Assertions......Page 56
3.2.3 Assertion Monitor Library Details......Page 61
3.2.4 Event Monitor & Assertion Checker Methodology......Page 62
3.2.4.2 Implementation Considerations......Page 64
3.2.4.3 Event Monitor Database & Analysis......Page 65
3.3 Summary......Page 66
Ch4 RTL Methodology Basics......Page 68
4.1 Simple RTL Verifiable Subset......Page 69
Recommendation: for Loop Construct......Page 72
Project Linting Principle......Page 73
4.2.1 Linting in Design Project......Page 74
4.2.2.1 Project Oriented......Page 75
4.2.2.2 Linting Message Examples......Page 76
4.3 Object-Based Hardware Design......Page 78
4.3.1 OBHD & Simulation......Page 81
4.3.2 OBHD & Formal Verification......Page 84
4.3.3.1 OBHD Synthesis......Page 85
4.3.3.2 OBHD Scan Chain Hookup......Page 87
4.3.4 Text Macro Implementation......Page 89
Object-Based Hardware Design Principle......Page 79
4.4 Summary......Page 92
Ch5 RTL Logic Simulation......Page 94
5.1.1 First Steps......Page 96
5.1.3 Function & Timing......Page 98
5.1.5 Acceleration & Emulation......Page 99
5.1.6 Language Standardization......Page 101
5.2 Project Simulation Phases......Page 103
5.2.1 Debugging Phase......Page 104
5.2.2 Performance Profiling Phase......Page 105
5.2.3 Regression Phase......Page 106
5.2.5 Performance......Page 107
5.3 Operation......Page 108
Visit Minimization Principle......Page 109
5.3.1.2 Rank-Ordered......Page 111
5.3.2.2 Compiled Code......Page 113
5.4 Optimizations......Page 114
5.4.3 Bus Reconstruction......Page 115
5.4.3.2 Expression Simplification......Page 116
5.4.5 Partitioning......Page 117
5.4.5.1 Branch Partitioning......Page 118
5.4.5.3 Chip Partitioning......Page 119
5.5.1.1 Design Method......Page 120
5.5.1.2 Zero Initialization......Page 121
5.5.1.3 Random Initialization......Page 122
5.5.2 Tri-State Buses......Page 123
5.5.3 Assertion Monitors......Page 124
5.6 Summary......Page 125
Ch6 RTL Formal Verification......Page 128
6.1 Formal Verification Introduction......Page 131
6.2 Finite State Machines......Page 132
6.2.1 Machine Equivalence......Page 135
6.2.2 FSM Property Verification......Page 136
6.3.1.1 Equivalence Checking Flow......Page 137
6.3.1.2 Closing Verification Loop......Page 139
6.3.2 Cutpoint Definition......Page 140
Cutpoint Identification Principle......Page 142
6.3.3.3 Equivalence Checking OBHD Practices......Page 143
6.3.4 RTL Static Sign-Off......Page 145
6.3.5 Effective Equivalence Checking Methodology......Page 147
6.4.1 Specification......Page 149
6.4.2 Model Checking & Parameterized Modules......Page 151
Numeric Value Parameterization Principle......Page 152
6.5 Summary......Page 153
Ch7 Verifiable RTL Style......Page 156
7.1.1 Asynchronous Logic......Page 157
Asynchronous Principle......Page 158
7.1.3 Combinational Feedback......Page 160
Combinational Feedback Principle......Page 162
7.1.4.1 Fully-Specified case Statements......Page 163
7.1.4.2 Test Signal & Constant Widths......Page 168
7.1.5 Tri-State Buses......Page 169
7.2.1.1 Compiler Options......Page 171
7.2.1.2 Design Hierarchy......Page 173
7.2.1.3 Files......Page 174
7.2.1.4 Libraries......Page 175
7.2.2.1 Overall Organization......Page 176
7.2.3 Expression Organization......Page 178
7.3.1.1 Consistency......Page 180
7.3.1.2 Upper/Lower Case......Page 181
7.3.1.3 Hierarchical Name References......Page 182
7.3.1.4 Global/Local Name Space......Page 183
7.3.1.5 Profiling Support......Page 184
7.3.2.3 Instances......Page 186
7.3.2.4 Modules......Page 187
7.3.2.5 Port Names......Page 188
7.3.2.6 Signal Names......Page 189
7.3.2.7 User Tasks/Functions & Program Libraries......Page 190
7.5 Editing Practices......Page 191
7.5.2 Comments......Page 192
7.5.2.2 Declarations......Page 193
7.5.2.4 Tool Controls......Page 194
Property Principle......Page 196
7.6 Summary......Page 197
Ch8 Bad Stuff......Page 198
8.1 In-Line Storage Element Specification......Page 199
8.2 RTL X-State......Page 200
8.2.1.1 RTL X-State Pessimism......Page 201
8.2.1.3 Impractical......Page 202
8.3.1 Bit Visits......Page 205
8.3.2 Configuration Test Visits......Page 206
8.3.3 for Loops......Page 207
Faithful Semantics Principle......Page 209
8.4.1.1 Full & Parallel Case......Page 210
8.4.1.2 X Assignment......Page 213
8.4.1.3 Other Forms of State Machines......Page 214
8.4.1.4 Initial Blocks......Page 215
8.4.2.1 Incomplete Sensitivity List......Page 216
8.4.2.3 Incorrect Procedural Statement Ordering......Page 217
8.4.3.1 Delays......Page 218
8.4.3.2 Race Conditions......Page 221
8.5.1 Linting & Problematic RTL Verilog......Page 223
8.5.3 Formal Verification & Problematic Verilog......Page 224
Good Vendor Principle......Page 225
8.6.1 Tool Library Function Naming......Page 226
8.6.2 Command Line Consistency......Page 227
8.6.3 Vendor Specific Properties......Page 228
8.7 Design Team Discipline......Page 229
8.8.2 Parameters......Page 230
8.8.3 User-Defined Primitives......Page 231
8.9 Summary......Page 232
Ch9 Verifiable RTL Tutorial......Page 234
9.1.1 Specification......Page 235
9.1.2 Comments......Page 236
9.1.4 Interconnection......Page 237
9.2 Adding Behavior......Page 240
9.3 Multi-Bit Interconnect & Behavior......Page 241
9.4 Parameters......Page 242
9.5.1.1 Binary Operators......Page 243
9.5.1.2 Unary Operators......Page 244
9.5.1.3 Miscellaneous Operators......Page 245
9.5.2 Operator Precedence......Page 246
9.6.1.1 Procedural Assignments......Page 247
9.6.1.2 Functions......Page 249
9.6.1.4 case, casex Statements......Page 250
9.6.2.1 Flip-Flops......Page 252
9.6.2.3 Memories......Page 253
9.6.3 Debugging......Page 254
9.6.3.1 $display & $write Statements......Page 255
9.7 Testbench......Page 256
9.8.1.1 Constants......Page 260
9.8.1.2 Code Inclusion......Page 261
9.8.1.3 Command Line......Page 262
9.9 Summary......Page 263
10.1 Principles......Page 264
10.1.4 Orthogonal Verification Principle......Page 265
10.1.7 Project Linting Principle......Page 266
10.1.11 Cutpoint Identification Principle......Page 267
10.1.13 Consistency Principle......Page 268
10.1.17 Faithful Semantics Principle......Page 269
10.2 Summary......Page 270
Bibliography......Page 272
AppA Comparing Verilog Construct Performance......Page 280
Lexical Elements......Page 284
Reserved Words......Page 285
Module Organization......Page 286
Procedural Statements......Page 287
Operators......Page 288
Compiler Directives......Page 289
AppC Assertion Monitors......Page 290
assert_always......Page 291
assert_change......Page 292
assert_window......Page 295
assert_frame......Page 297
Index......Page 302
