Borrow it
 African Studies Library
 Alumni Medical Library
 Astronomy Library
 Fineman and Pappas Law Libraries
 Frederick S. Pardee Management Library
 Howard Gotlieb Archival Research Center
 Mugar Memorial Library
 Music Library
 Pikering Educational Resources Library
 School of Theology Library
 Science & Engineering Library
 Stone Science Library
The Resource Formal Verification of FloatingPoint Hardware Design : A Mathematical Approach, by David M. Russinoff, (electronic resource)
Formal Verification of FloatingPoint Hardware Design : A Mathematical Approach, by David M. Russinoff, (electronic resource)
Resource Information
The item Formal Verification of FloatingPoint Hardware Design : A Mathematical Approach, by David M. Russinoff, (electronic resource) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in Boston University Libraries.This item is available to borrow from all library branches.
Resource Information
The item Formal Verification of FloatingPoint Hardware Design : A Mathematical Approach, by David M. Russinoff, (electronic resource) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in Boston University Libraries.
This item is available to borrow from all library branches.
 Summary
 This is the first book to focus on the problem of ensuring the correctness of floatingpoint hardware designs through mathematical methods. Formal Verification of FloatingPoint Hardware Design advances a verification methodology based on a unified theory of registertransfer logic and floatingpoint arithmetic that has been developed and applied to the formal verification of commercial floatingpoint units over the course of more than two decades, during which the author was employed by several major microprocessor design companies. 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 fixedpoint encodings, and bitwise logical operations. Part II addresses the properties of floatingpoint numbers, the formats in which they are encoded as bit vectors, and the various modes of floatingpoint rounding. 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. As a basis for the formal verification of such implementations, Part IV contains highlevel specifications of correctness of the basic arithmetic instructions of several major industrystandard floatingpoint architectures, including all details pertaining to the handling of exceptional conditions. Part V illustrates the methodology, applying the preceding theory to the comprehensive verification of a stateoftheart commercial floatingpoint unit. All of these results have been formalized in the logic of the ACL2 theorem prover and mechanically checked to ensure their correctness. They are presented here, however, in simple conventional mathematical notation. The book presupposes no familiarity with ACL2, logic design, or any mathematics beyond basic high school algebra. 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.
 Language
 eng
 Extent
 XXIV, 382 p. 32 illus.
 Contents

 1 Basic Arithmetic Functions
 2 Bit Vectors
 3 Logical Operations
 4 FloatingPoint Numbers
 5 FloatingPoint Formats
 6 Rounding
 7 IEEECompliant Square Root
 8 Addition
 9 Multiplication
 10 SRT Division and Square Root
 11 FMABased Division
 12 SSE FloatingPoint Instructions
 13 x87 Instructions
 14 Arm FloatingPoint Instructions
 15 The Modeling Language
 16 DoublePrecision Multiplication
 17 DoublePrecision Addition and FMA
 18 MultiPrecision Radix4 SRT Division
 19 MultiPrecision Radix4 SRT Square Root
 Isbn
 9783319955131
 Label
 Formal Verification of FloatingPoint Hardware Design : A Mathematical Approach
 Title
 Formal Verification of FloatingPoint Hardware Design
 Title remainder
 A Mathematical Approach
 Statement of responsibility
 by David M. Russinoff
 Subject

 Software engineering
 Processor Architectures
 Computer science
 Computer science
 Software engineering
 Operating systems (Computers)
 Software Engineering
 Systems engineering
 Systems engineering
 Electronic resources
 Systems engineering
 Circuits and Systems
 Operating systems (Computers)
 Software engineering
 Operating systems (Computers)
 Software Engineering
 Performance and Reliability
 Computer science
 Software Engineering
 Language
 eng
 Summary
 This is the first book to focus on the problem of ensuring the correctness of floatingpoint hardware designs through mathematical methods. Formal Verification of FloatingPoint Hardware Design advances a verification methodology based on a unified theory of registertransfer logic and floatingpoint arithmetic that has been developed and applied to the formal verification of commercial floatingpoint units over the course of more than two decades, during which the author was employed by several major microprocessor design companies. 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 fixedpoint encodings, and bitwise logical operations. Part II addresses the properties of floatingpoint numbers, the formats in which they are encoded as bit vectors, and the various modes of floatingpoint rounding. 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. As a basis for the formal verification of such implementations, Part IV contains highlevel specifications of correctness of the basic arithmetic instructions of several major industrystandard floatingpoint architectures, including all details pertaining to the handling of exceptional conditions. Part V illustrates the methodology, applying the preceding theory to the comprehensive verification of a stateoftheart commercial floatingpoint unit. All of these results have been formalized in the logic of the ACL2 theorem prover and mechanically checked to ensure their correctness. They are presented here, however, in simple conventional mathematical notation. The book presupposes no familiarity with ACL2, logic design, or any mathematics beyond basic high school algebra. 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.
 http://library.link/vocab/creatorName
 Russinoff, David M
 http://bibfra.me/vocab/relation/httpidlocgovvocabularyrelatorsaut
 lNjD3GiLLA8
 Image bit depth
 0
 LC call number
 TK7888.4
 Literary form
 non fiction
 http://library.link/vocab/relatedWorkOrContributorName
 SpringerLink
 http://library.link/vocab/subjectName

 Systems engineering
 Software engineering
 Computer science
 Operating systems (Computers)
 Circuits and Systems
 Software Engineering
 Processor Architectures
 Performance and Reliability
 Label
 Formal Verification of FloatingPoint Hardware Design : A Mathematical Approach, by David M. Russinoff, (electronic resource)
 Antecedent source
 mixed
 Carrier category
 online resource
 Carrier category code
 cr
 Carrier MARC source
 rdacarrier
 Color
 not applicable
 Content category
 text
 Content type code
 txt
 Content type MARC source
 rdacontent
 Contents
 1 Basic Arithmetic Functions  2 Bit Vectors  3 Logical Operations  4 FloatingPoint Numbers  5 FloatingPoint Formats  6 Rounding  7 IEEECompliant Square Root  8 Addition  9 Multiplication  10 SRT Division and Square Root  11 FMABased Division  12 SSE FloatingPoint Instructions  13 x87 Instructions  14 Arm FloatingPoint Instructions  15 The Modeling Language  16 DoublePrecision Multiplication  17 DoublePrecision Addition and FMA  18 MultiPrecision Radix4 SRT Division  19 MultiPrecision Radix4 SRT Square Root
 Dimensions
 unknown
 Extent
 XXIV, 382 p. 32 illus.
 File format
 multiple file formats
 Form of item
 electronic
 Isbn
 9783319955131
 Level of compression
 uncompressed
 Media category
 computer
 Media MARC source
 rdamedia
 Media type code
 c
 Other control number
 10.1007/9783319955131
 Other physical details
 online resource.
 Quality assurance targets
 absent
 Reformatting quality
 access
 Specific material designation
 remote
 System control number
 (DEHe213)9783319955131
 Label
 Formal Verification of FloatingPoint Hardware Design : A Mathematical Approach, by David M. Russinoff, (electronic resource)
 Antecedent source
 mixed
 Carrier category
 online resource
 Carrier category code
 cr
 Carrier MARC source
 rdacarrier
 Color
 not applicable
 Content category
 text
 Content type code
 txt
 Content type MARC source
 rdacontent
 Contents
 1 Basic Arithmetic Functions  2 Bit Vectors  3 Logical Operations  4 FloatingPoint Numbers  5 FloatingPoint Formats  6 Rounding  7 IEEECompliant Square Root  8 Addition  9 Multiplication  10 SRT Division and Square Root  11 FMABased Division  12 SSE FloatingPoint Instructions  13 x87 Instructions  14 Arm FloatingPoint Instructions  15 The Modeling Language  16 DoublePrecision Multiplication  17 DoublePrecision Addition and FMA  18 MultiPrecision Radix4 SRT Division  19 MultiPrecision Radix4 SRT Square Root
 Dimensions
 unknown
 Extent
 XXIV, 382 p. 32 illus.
 File format
 multiple file formats
 Form of item
 electronic
 Isbn
 9783319955131
 Level of compression
 uncompressed
 Media category
 computer
 Media MARC source
 rdamedia
 Media type code
 c
 Other control number
 10.1007/9783319955131
 Other physical details
 online resource.
 Quality assurance targets
 absent
 Reformatting quality
 access
 Specific material designation
 remote
 System control number
 (DEHe213)9783319955131
Subject
 Circuits and Systems
 Computer science
 Computer science
 Computer science
 Electronic resources
 Operating systems (Computers)
 Operating systems (Computers)
 Operating systems (Computers)
 Performance and Reliability
 Processor Architectures
 Software Engineering
 Software Engineering
 Software Engineering
 Software engineering
 Software engineering
 Software engineering
 Systems engineering
 Systems engineering
 Systems engineering
Library Locations

African Studies LibraryBorrow it771 Commonwealth Avenue, 6th Floor, Boston, MA, 02215, US42.350723 71.108227


Astronomy LibraryBorrow it725 Commonwealth Avenue, 6th Floor, Boston, MA, 02445, US42.350259 71.105717

Fineman and Pappas Law LibrariesBorrow it765 Commonwealth Avenue, Boston, MA, 02215, US42.350979 71.107023

Frederick S. Pardee Management LibraryBorrow it595 Commonwealth Avenue, Boston, MA, 02215, US42.349626 71.099547

Howard Gotlieb Archival Research CenterBorrow it771 Commonwealth Avenue, 5th Floor, Boston, MA, 02215, US42.350723 71.108227


Music LibraryBorrow it771 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US42.350723 71.108227

Pikering Educational Resources LibraryBorrow it2 Silber Way, Boston, MA, 02215, US42.349804 71.101425

School of Theology LibraryBorrow it745 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US42.350494 71.107235

Science & Engineering LibraryBorrow it38 Cummington Mall, Boston, MA, 02215, US42.348472 71.102257

Embed (Experimental)
Settings
Select options that apply then copy and paste the RDF/HTML data fragment to include in your application
Embed this data in a secure (HTTPS) page:
Layout options:
Include data citation:
<div class="citation" vocab="http://schema.org/"><i class="fa faexternallinksquare fafw"></i> Data from <span resource="http://link.bu.edu/portal/FormalVerificationofFloatingPointHardware/nCUouVEB04k/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.bu.edu/portal/FormalVerificationofFloatingPointHardware/nCUouVEB04k/">Formal Verification of FloatingPoint Hardware Design : A Mathematical Approach, by David M. Russinoff, (electronic resource)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.bu.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.bu.edu/">Boston University Libraries</a></span></span></span></span></div>
Note: Adjust the width and height settings defined in the RDF/HTML code fragment to best match your requirements
Preview
Cite Data  Experimental
Data Citation of the Item Formal Verification of FloatingPoint Hardware Design : A Mathematical Approach, by David M. Russinoff, (electronic resource)
Copy and paste the following RDF/HTML data fragment to cite this resource
<div class="citation" vocab="http://schema.org/"><i class="fa faexternallinksquare fafw"></i> Data from <span resource="http://link.bu.edu/portal/FormalVerificationofFloatingPointHardware/nCUouVEB04k/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.bu.edu/portal/FormalVerificationofFloatingPointHardware/nCUouVEB04k/">Formal Verification of FloatingPoint Hardware Design : A Mathematical Approach, by David M. Russinoff, (electronic resource)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.bu.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.bu.edu/">Boston University Libraries</a></span></span></span></span></div>