Formal Verification of Floating-Point Hardware Design : A Mathematical Approach

ISBN-13: 9783319955124 / Angielski / Twarda / 2018 / 382 str.

David M. Russinoff; J. Strother Moore

Spis treści

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.

O autorze

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.  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.