Bit-vectors
Libraries for reasoning about bit vectors.
Subtopics
- Sparseint
- Alternative implementation of bignums based on balanced binary trees
- Bitops
- Bitops is a library originally developed at Centaur Technology
for reasoning about bit-vector arithmetic. It grew out of an extension
to the venerable ACL2::ihs library, and is now fairly comprehensive.
- Bv
- The BV library for reasoning about bit-vectors
- Ihs
- The Integer Hardware Specification (IHS) library is a collection of
arithmetic books, mainly geared toward bit-vector arithmetic.
- Rtl
- A library of register-transfer logic and computer arithmetic
