Abstract
Many of the preceding results are propositions pertaining to real variables, which are formalized by ACL2 events in which these variables are restricted to the rational domain. Many of the lemmas of this chapter similarly apply to arbitrary real numbers, but in light of our present focus, these results are formulated to correspond more closely with their formal versions. Apart from the informal discussion immediately below, the lemmas themselves contain no references to the real numbers or the square root function.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsAuthor information
Authors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Russinoff, D.M. (2019). IEEE-Compliant Square Root. In: Formal Verification of Floating-Point Hardware Design. Springer, Cham. https://doi.org/10.1007/978-3-319-95513-1_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-95513-1_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-95512-4
Online ISBN: 978-3-319-95513-1
eBook Packages: EngineeringEngineering (R0)