Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Recursion-and-induction
Boolean-reasoning
Debugging
Projects
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
Multiplication
FMA-Based Division
Addition
SRT Division and Square Root
SRT Division and Quotient Digit Selection
SRT Square Root Extraction
Register-Transfer Logic
Floating-Point Arithmetic
Modeling Algorithms in C++ and ACL2
Bibliography
Algebra
Testing-utilities
Implementation of Elementary Operations
SRT Division and Square Root
SRT Division and Square Root
Subtopics
SRT Division and Quotient Digit Selection
SRT Division and Quotient Digit Selection
SRT Square Root Extraction
SRT Square Root Extraction