Details

Formal Verification of Floating-Point Hardware Design


Formal Verification of Floating-Point Hardware Design

A Mathematical Approach

von: David M. Russinoff, J Strother Moore

90,94 €

Verlag: Springer
Format: PDF
Veröffentl.: 13.10.2018
ISBN/EAN: 9783319955131
Sprache: englisch

Dieses eBook enthält ein Wasserzeichen.

Beschreibungen

<p>This is the first book to focus on the problem of ensuring the correctness of floating-point hardware designs through mathematical methods.&nbsp; <i>Formal Verification of Floating-Point Hardware Design</i> 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.</p>

<p>&nbsp;The book consists of five parts, the first two of which present a rigorous exposition of the general theory based on the first principles of arithmetic. Part I covers bit vectors and the bit manipulation primitives, integer and fixed-point encodings, and bit-wise logical operations.&nbsp; Part II addresses the properties of floating-point numbers, the formats in which they are encoded as bit vectors, and the various modes of floating-point rounding.&nbsp; In Part III, the theory is extended to the analysis of several algorithms and optimization techniques that are commonly used in commercial implementations of elementary arithmetic operations.&nbsp; As a basis for the formal verification of such implementations, Part IV contains high-level specifications of correctness of the basic arithmetic instructions of several major industry-standard floating-point architectures, including all details pertaining to the handling of exceptional conditions.&nbsp; Part V illustrates the methodology, applying the preceding theory to the comprehensive verification of a state-of-the-art commercial floating-point unit.</p><p>&nbsp;All of these results have been formalized in the logic of the ACL2 theorem prover and mechanically checked to ensure their correctness.&nbsp; They are presented here, however, in simple conventional mathematical notation.&nbsp; The book presupposes no familiarity with ACL2, logic design, or any mathematics beyond basic high school algebra.&nbsp; It will be of interest to verification engineers as well as arithmetic circuit designers who appreciate the value of a rigorous approach to their art, and is suitable as a graduate text in computer arithmetic.</p><p></p><p></p>

<p>&nbsp;</p>

<p><br></p>
1 Basic Arithmetic Functions.- 2 Bit Vectors.- 3 Logical Operations.- 4 Floating-Point Numbers.- 5 Floating-Point Formats.- 6 Rounding.- 7 IEEE-Compliant Square Root.- 8 Addition.- 9 Multiplication.- 10 SRT Division and Square Root.- 11 FMA-Based Division.- 12 SSE Floating-Point Instructions.- 13 x87 Instructions.- 14 Arm Floating-Point Instructions.- 15 The Modeling Language.- 16 Double-Precision Multiplication.- 17 Double-Precision Addition and FMA.- 18 Multi-Precision Radix-4 SRT Division.- 19 Multi-Precision Radix-4 SRT Square Root.
<p></p>David M. Russinoff is Principal Engineer at Arm Holdings. He holds a bachelor's degree from the Massachusetts Institute of Technology and a doctorate from New York University, both in mathematics, and a master's in computer sciences from the University of Texas at Austin.&nbsp; He has spent twenty-five years developing mathematical methods of hardware verification, with an emphasis on interactive theorem proving, and applying them in the analysis of commercial designs, especially arithmetic circuits.&nbsp;&nbsp;
A unified mathematical theory of register-transfer logic and computer arithmetic Analysis of a collection of algorithms and optimization techniques commonly used in commercial implementations Comprehensive behavioral specifications of the elementary arithmetic instructions of a variety of industry-standard architectures A verification methodology combining interactive theorem proving with sequential logic equivalence checking Illustrated through the formal verification of a state-of-the-art commercial floating-point unit

Diese Produkte könnten Sie auch interessieren:

Pulsed Power
Pulsed Power
von: Gennady A. Mesyats
PDF ebook
309,23 €
High-Frequency Oscillator Design for Integrated Transceivers
High-Frequency Oscillator Design for Integrated Transceivers
von: J. van der Tang, Dieter Kasperkovitz, Arthur H.M. van Roermund
PDF ebook
149,79 €
MEMS Vibratory Gyroscopes
MEMS Vibratory Gyroscopes
von: Cenk Acar, Andrei Shkel
PDF ebook
149,79 €