| 书目名称 | Formal Verification of Floating-Point Hardware Design |
| 副标题 | A Mathematical Appro |
| 编辑 | David M. Russinoff |
| 视频video | http://file.papertrans.cn/346/345954/345954.mp4 |
| 概述 | 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.Comprehe |
| 图书封面 |  |
| 描述 | .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. 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 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. 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. 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 |
| 出版日期 | Book 20191st edition |
| 关键词 | floating-point arithmetic; interactive theorem proving; ACL2; formal verification; computer aritmetic; SR |
| 版次 | 1 |
| doi | https://doi.org/10.1007/978-3-319-95513-1 |
| isbn_softcover | 978-3-030-07048-9 |
| isbn_ebook | 978-3-319-95513-1 |
| copyright | Springer Nature Switzerland AG 2019 |
|Archiver|手机版|小黑屋|
派博传思国际
( 京公网安备110108008328)
GMT+8, 2025-8-2 09:01
发表于 2025-3-21 18:15:34
