		Search-engine friendly clone of the ACL2 documentation.

Rtl

A library of register-transfer logic and computer arithmetic

This documentation is based on the directory rtl of the ACL2 community-books. For a more thorough treatment, see "Formal Verification of Floating-Point Hardware Design: A Mathematical Approach" by David M. Russinoff. See file rtl/README for additional information about this library and its connection to this book.

Floating-Point Exceptions and Specification of Elementary Arithmetic Instructions: Floating-Point Exceptions and Specification of Elementary Arithmetic Instructions
Implementation of Elementary Operations: Implementation of Elementary Operations
Register-Transfer Logic: Register-Transfer Logic
Floating-Point Arithmetic: Floating-Point Arithmetic
Modeling Algorithms in C++ and ACL2: Modeling Algorithms in C++ and ACL2
Bibliography: Bibliography