Logical reverse. (logrev size i) bit-reverses the size
low-order bits of i, discarding the high-order bits.
(logrev size i) → nat
- size — Guard (and (integerp size) (<= 0 size)).
- i — Guard (integerp i).
- nat — Type (natp nat).
Normally we don't think of bit-reversing as a logical operation,
even though its hardware implementation is trivial: simply reverse the wires
leading from the source to the destination.
logrev is included as a logical operation to support the specification
of DSPs, which may provide bit-reversing in their address generators to improve
the performance of the FFT.
logrev entails a recursive definition of bit-reversing via the helper
See also bitops::bitops/fast-logrev for some optimized definitions of
Definitions and Theorems
(defun logrev$inline (size i)
(declare (xargs :guard (and (and (integerp size) (<= 0 size))
(let ((__function__ 'logrev))
(declare (ignorable __function__))
(logrev1 size i 0)))
(b* ((nat (logrev$inline size i)))
- Helper function for logrev.
- Optimized definitions of logrev at particular sizes.