مشخصات کتاب

Higher Order Logic and Hardware Verification

ویرایش:  
نویسندگان: Melham T.F.  
سری: Cambridge Tracts in Theoretical Computer Science 31 
ISBN (شابک) : 9780521417181, 9780521115322 
ناشر: Cambridge University Press 
سال نشر: 1993 
تعداد صفحات: 180 
زبان: English 
فرمت فایل : DJVU (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 2 مگابایت 

در صورت ایرانی بودن نویسنده امکان دانلود وجود ندارد و مبلغ عودت داده خواهد شد

در صورت تبدیل فایل کتاب Higher Order Logic and Hardware Verification به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.

توجه داشته باشید کتاب منطق سفارش بالاتر و تأیید سخت افزار نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.

توضیحاتی در مورد کتاب منطق سفارش بالاتر و تأیید سخت افزار

دکتر ملهام در اینجا نشان می دهد که چگونه می توان از منطق رسمی برای مشخص کردن رفتار طراحی های سخت افزاری و دلیل درستی آنها استفاده کرد. موضوع اصلی کتاب استفاده از انتزاع در مشخصات سخت افزاری و تأیید است. نویسنده توضیح می‌دهد که چگونه برخی مکانیسم‌های انتزاعی اساسی برای تأیید سخت‌افزار را می‌توان در منطق رسمی‌سازی کرد و برای بیان ادعاهایی درباره صحت طراحی و دقت نسبی مدل‌های رفتار سخت‌افزار استفاده کرد. رویکرد او عمل گرایانه و مبتنی بر مثال است. او همچنین مقدمه‌ای بر منطق مرتبه بالاتر، که یک فرمالیسم پرکاربرد در این موضوع است، ارائه می‌کند و توضیح می‌دهد که چگونه این فرمالیسم در واقع برای تأیید سخت‌افزار استفاده می‌شود. این کتاب تا حدی بر اساس تحقیقات خود نویسنده و همچنین آموزش فارغ التحصیلان است. بنابراین می توان از آن برای همراهی دوره های تأیید سخت افزار و به عنوان منبعی برای پژوهشگران استفاده کرد

توضیحاتی درمورد کتاب به خارجی

Dr. Melham shows here how formal logic can be used to specify the behavior of hardware designs and reason about their correctness. A primary theme of the book is the use of abstraction in hardware specification and verification. The author describes how certain fundamental abstraction mechanisms for hardware verification can be formalized in logic and used to express assertions about design correctness and the relative accuracy of models of hardware behavior. His approach is pragmatic and driven by examples. He also includes an introduction to higher-order logic, which is a widely used formalism in this subject, and describes how that formalism is actually used for hardware verification. The book is based in part on the author's own research as well as on graduate teaching. Thus it can be used to accompany courses on hardware verification and as a resource for research workers

فهرست مطالب

Cover......Page 1
Frontmatter......Page 2
Contents......Page 6
List of Figures......Page 10
Preface......Page 12
1 - Hardware Verification......Page 16
1.1 The hardware verification method......Page 17
1.2 Limitations of hardware verification......Page 18
1.3 Abstraction......Page 19
1.4 Hardware verification using higher order logic......Page 21
2.1 Types......Page 24
2.2 Terms......Page 27
2.3 Sequents, theorems and inference rules......Page 31
2.4 Constant definitions......Page 33
2.5 The primitive constant [ELEMENT OF]......Page 34
2.6 Recursive definitions......Page 35
2.7 Type definitions......Page 36
2.8 The HOL system......Page 39
3.1 Specifying hardware behaviour......Page 44
3.2 Deriving behaviour from structure......Page 50
3.3 Formulating correctness......Page 53
3.4 An example correctness proof......Page 54
3.5 Other approaches......Page 57
4 - Abstraction......Page 62
4.1 Abstraction within a model......Page 63
4.2 Two problems......Page 69
4.3 Abstraction in practice......Page 71
4.4 Validity conditions......Page 73
4.5 A notation for correctness......Page 74
4.6 Abstraction and hierarchical verification......Page 75
4.7 Abstraction between models......Page 81
4.8 Other approaches......Page 83
5.1 Defining concrete types in logic......Page 84
5.2 An example: a transistor model......Page 89
5.3 An example of data abstraction......Page 92
5.4 Reasoning about hardware using bit-vectors......Page 97
5.5 Reasoning about tree-shaped circuits......Page 103
5.6 Other approaches......Page 109
6.1 Temporal abstraction by sampling......Page 112
6.2 An example: abstracting to unit delay......Page 118
6.3 A synchronizing temporal abstraction......Page 120
6.4 A case study: the T-ring......Page 121
6.5 Other approaches......Page 140
7.1 Representing the structure of CMOS circuits......Page 144
7.2 Defining the semantics of CMOS circuits......Page 148
7.4 Correctness in the two models......Page 151
7.5 Relating the models......Page 153
7.6 Improving the results......Page 158
7.7 Other approaches......Page 161
References......Page 162
Index......Page 174

نظرات کاربران

کتاب های تصادفی

دانلود کتاب Infection Control: Dilemmas and Practical Solutions

دانلود کتاب 1949: The First Israelis

دانلود کتاب Wie aus Zahlen Bilder werden: Wirtschaftsdaten Überzeugend Präsentiert

دانلود کتاب How To Practice Shamatha Meditation: The Cultivation Of Meditative Quiescence

دانلود کتاب Integrating project delivery