Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
100-theorems
Arithmetic
Bit-vectors
Sparseint
Bitops
Bv
Ihs
Rtl
Floating-Point Exceptions and Specification of Elementary Arithmetic Instructions
Implementation of Elementary Operations
Register-Transfer Logic
Floating-Point Arithmetic
Rounding
Unbiased Rounding
IEEE Rounding
Denormal Rounding
Rounding Away from Zero
Truncation
Odd Rounding
Floating-Point Formats
Floating-Point Numbers
Modeling Algorithms in C++ and ACL2
Bibliography
Algebra
Testing-utilities
Floating-Point Arithmetic
Rounding
Rounding
Subtopics
Unbiased Rounding
Unbiased Rounding
IEEE Rounding
IEEE Rounding
Denormal Rounding
Denormal Rounding
Rounding Away from Zero
Rounding Away from Zero
Truncation
Truncation
Odd Rounding
Odd Rounding