دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
دانلود کتاب Formal verification of floating-point hardware design : a mathematical approach
دانلود کتاب تأیید رسمی طراحی سخت افزار ممیز شناور: یک رویکرد ریاضی
مشخصات کتاب
Formal verification of floating-point hardware design : a mathematical approach
ویرایش: Second
نویسندگان: David Russinoff
سری:
ISBN (شابک) : 9783030871819, 3030871819
ناشر:
سال نشر: 2022
تعداد صفحات: 448
زبان: English
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود)
حجم فایل: 5 مگابایت
قیمت کتاب (تومان) : 39,000
در صورت تبدیل فایل کتاب Formal verification of floating-point hardware design : a mathematical approach به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب تأیید رسمی طراحی سخت افزار ممیز شناور: یک رویکرد ریاضی نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
توضیحاتی در مورد کتاب تأیید رسمی طراحی سخت افزار ممیز شناور: یک رویکرد ریاضی
این اولین کتابی است که بر روی مسئله اطمینان از صحت طراحی های سخت افزاری ممیز شناور از طریق روش های ریاضی تمرکز می کند. تأیید رسمی طراحی سخت‌افزار ممیز شناور، ویرایش دوم یک روش تأیید را بر اساس یک نظریه یکپارچه منطق ثبت-انتقال و محاسبات ممیز شناور که برای تأیید رسمی واحدهای ممیز شناور تجاری در طول دوره توسعه یافته و اعمال شده است، ارائه می‌کند. بیش از دو دهه، که در طی آن نویسنده توسط چندین شرکت بزرگ طراحی ریزپردازنده به کار گرفته شد. این تئوری به تجزیه و تحلیل چندین الگوریتم و تکنیک‌های بهینه‌سازی که معمولاً در پیاده‌سازی تجاری عملیات‌های حسابی ابتدایی استفاده می‌شوند، گسترش یافته است. به عنوان مبنایی برای تأیید رسمی چنین پیاده‌سازی‌هایی، مشخصات سطح بالا دستورالعمل‌های محاسباتی پایه چندین معماری ممیز شناور استاندارد صنعتی، از جمله تمام جزئیات مربوط به رسیدگی به شرایط استثنایی ارائه شده است. این روش در راستی‌آزمایی جامع انواع پیشرفته‌ترین طرحهای ممیز شناور تجاری توسعه‌یافته توسط Arm Holdings نشان داده شده است. این نسخه اصلاح شده، ریزمعماری در حال تکامل و پیچیدگی روزافزون پردازنده های Arm، و تنوع در اهداف طراحی سرعت اجرا، نیازمندی های ناحیه سخت افزاری و مصرف انرژی را منعکس می کند. بسیاری از نتایج جدید به بخش I-III (منطق ثبت-انتقال، محاسبات ممیز شناور، و اجرای عملیات ابتدایی) اضافه شده است، که تئوری را گسترش داده و تکنیک های جدید را توصیف می کند. اینها همانطور که در راستی آزمایی طرحهای جدید RTL شرح داده شده در قسمت V مشتق شدند.
توضیحاتی درمورد کتاب به خارجی
This is the first book to focus on the problem of ensuring the correctness of floating-point hardware designs through mathematical methods. Formal Verification of Floating-Point Hardware Design, Second Edition advances a verification methodology based on a unified theory of register-transfer logic and floating-point arithmetic that has been developed and applied to the formal verification of commercial floating-point units over the course of more than two decades, during which the author was employed by several major microprocessor design companies. The theory is extended to the analysis of several algorithms and optimization techniques that are commonly used in commercial implementations of elementary arithmetic operations. As a basis for the formal verification of such implementations, high-level specifications of the basic arithmetic instructions of several major industry-standard floating-point architectures are presented, including all details pertaining to the handling of exceptional conditions. The methodology is illustrated in the comprehensive verification of a variety of state-of-the-art commercial floating-point designs developed by Arm Holdings. This revised edition reflects the evolving microarchitectures and increasing sophistication of Arm processors, and the variation in the design goals of execution speed, hardware area requirements, and power consumption. Many new results have been added to Parts I—III (Register-Transfer Logic, Floating-Point Arithmetic, and Implementation of Elementary Operations), extending the theory and describing new techniques. These were derived as required in the verification of the new RTL designs described in Part V.
فهرست مطالب
Foreword Preface to the Second Edition Preface to the First Edition Contents and Structure of the Book Formalization: The Role of ACL2 Obtaining the Associated ACL2 Code Acknowledgments Contents Part I Register-Transfer Logic 1 Basic Arithmetic Functions 1.1 Floor and Ceiling 1.2 Modulus 1.3 Truncation 2 Bit Vectors 2.1 Bit Slices 2.2 Bit Extraction 2.3 Concatenation 2.4 Integer Formats 2.5 Fixed-Point Formats 3 Logical Operations 3.1 Binary Operations 3.2 Complement Part II Floating-Point Arithmetic 4 Floating-Point Numbers 4.1 Decomposition 4.2 Exactness 5 Floating-Point Formats 5.1 Classification of Formats 5.2 Normal Encodings 5.3 Denormals and Zeroes 5.4 Infinities and NaNs 6 Rounding 6.1 Rounding Toward Zero 6.2 Rounding Away from Zero 6.3 Rounding to Nearest 6.4 Odd Rounding 6.5 IEEE Rounding 6.6 Denormal Rounding 6.7 Underflow Detection 7 IEEE-Compliant Square Root 7.1 Truncated Square Root 7.2 Odd-Rounded Square Root 7.3 IEEE-Rounded Square Root Part III Implementation of Elementary Operations 8 Addition 8.1 Bit Vector Addition 8.2 Parallel Prefix Adders 8.3 Leading Zero Anticipation 8.4 Counting Leading Zeroes 9 Multiplication 9.1 Radix-2 Booth Encoding 9.2 Radix-4 Booth Encoding 9.3 Encoding Carry-Save Sums 9.4 Statically Encoded Multiplier Arrays 9.5 Radix-8 Booth Encoding 10 SRT Division and Square Root 10.1 SRT Division 10.2 Minimally Redundant Radix-4 Division 10.3 Minimally Redundant Radix-8 Division 10.4 SRT Square Root 10.5 Minimally Redundant Radix-4 Square Root 10.6 Minimally Redundant Radix-8 Square Root 11 Division Based on Fused Multiply-Add 11.1 Reciprocal Approximation 11.2 Quotient Refinement 11.3 Reciprocal Refinement 11.4 Examples Part IV Comparative Architectures: SSE, x87, and Arm 12 SSE Floating-Point Instructions 12.1 SSE Control and Status Register 12.2 Overview of SSE Floating-Point Exceptions 12.3 Pre-computation Exceptions 12.4 Computation 12.5 Post-computation Exceptions 13 x87 Instructions 13.1 x87 Control Word 13.2 x87 Status Word 13.3 Overview of x87 Exceptions 13.4 Pre-computation Exceptions 13.5 Post-computation Exceptions 14 Arm Floating-Point Instructions 14.1 Floating-Point Status and Control Register 14.2 Pre-computation Exceptions 14.3 Post-computation Exceptions Part V Formal Verification of RTL Designs 15 The RAC Modeling Language 15.1 Language Overview 15.2 Parameter Passing 15.3 Registers 15.4 Arithmetic 15.5 Control Restrictions 15.6 Translation to ACL2 16 Double-Precision Multiplication and Scaling 16.1 Parameters 16.2 Booth Multiplier 16.3 Unrounded Product 16.4 FMA Support 16.5 Rounded Product: FMUL and FSCALE 17 Double-Precision Addition and Fused Multiply-Add 17.1 Preliminary Analysis 17.2 Alignment 17.3 Addition 17.4 Leading Zero Anticipation 17.5 Normalization 17.6 Rounding 17.7 Correctness Theorems 18 Multi-precision Radix-8 SRT Division 18.1 Overview 18.2 Pre-processing 18.3 Iterative Phase 18.4 Post-processing and Rounding 19 64-Bit Integer Division 19.1 Preliminary Analysis and Early Exit 19.2 Detecting Powers of 2 19.3 Instantiating the SRT Algorithm 19.4 Post-processing 20 Multi-precision Radix-4 SRT Square Root 20.1 Pre-processing 20.2 Iterative Phase 20.3 Post-processing and Rounding 21 Multi-precision Radix-2 SRT Division 21.1 Overview 21.2 Pre-processing 21.3 Iterative Phase 21.4 Post-processing 22 Fused Multiply-Add of a Graphics Processor 22.1 Overview 22.2 Multiplication 22.3 Rescaling 22.4 Addition 22.5 Final Result Bibliography Index
نظرات کاربران
کتاب های تصادفی
دانلود کتاب In Search of Structural Power
