Logrev
Logical reverse. (logrev size i) bit-reverses the size
low-order bits of i, discarding the high-order bits.
- Signature
(logrev size i) → nat
- Arguments
- size — Guard (and (integerp size) (<= 0 size)).
- i — Guard (integerp i).
- Returns
- 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
function logrev1.
See also bitops::bitops/fast-logrev for some optimized definitions of
logrev.
Definitions and Theorems
Function: logrev$inline
(defun logrev$inline (size i)
(declare (xargs :guard (and (and (integerp size) (<= 0 size))
(integerp i))))
(let ((__function__ 'logrev))
(declare (ignorable __function__))
(logrev1 size i 0)))
Theorem: logrev-type
(defthm logrev-type
(b* ((nat (logrev$inline size i)))
(natp nat))
:rule-classes :type-prescription)
Subtopics
- Logrev1
- Helper function for logrev.
- Bitops/fast-logrev
- Optimized definitions of logrev at particular sizes.
- Logrev-basics
