Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Gl
Esim
Vl2014
Sv
Vwsim
Fgl
Vl
X86isa
Svl
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
Software-verification
Math
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