• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
      • 100-theorems
      • Arithmetic
      • Bit-vectors
        • Sparseint
        • Bitops
          • Bitops/merge
          • Bitops-compatibility
          • Bitops-books
          • Logbitp-reasoning
          • Bitops/signed-byte-p
          • Fast-part-select
          • Bitops/integer-length
          • Bitops/extra-defs
          • Install-bit
          • Trailing-0-count
          • Bitops/defaults
          • Logbitp-mismatch
          • Trailing-1-count
          • Bitops/rotate
          • Bitops/equal-by-logbitp
          • Bitops/ash-bounds
          • Bitops/fast-logrev
          • Limited-shifts
          • Bitops/part-select
          • Bitops/parity
          • Bitops/saturate
            • Signed-saturate
              • Signed-saturate-fn
              • Signed-saturate64
              • Signed-saturate32
              • Signed-saturate16
              • Signed-saturate8
            • Unsigned-saturate
          • Bitops/part-install
          • Bitops/logbitp-bounds
          • Bitops/ihsext-basics
          • Bitops/fast-rotate
          • Bitops/fast-logext
          • Bitops/ihs-extensions
        • Bv
        • Ihs
        • Rtl
      • Algebra
    • Testing-utilities
  • Bitops/saturate

Signed-saturate

(signed-saturate n x) coerces the integer x into an n-bit signed integer by signed saturation, then returns the result as an n-bit unsigned number.

Normally signed saturation to n bits is understood as:

  • If x is too small (less than -2^{n-1}) it becomes -2^{n-1}.
  • If x is too big (2^{n-1} or more) it becomes 2^{n-1} - 1.
  • Otherwise x is unchanged.

This is almost what we compute. The twist is: after saturating as above, we mask the above with 2^{n-1} to obtain an unsigned, n-bit result.

signed-saturate is actually a macro. Generally it expands into a call of signed-saturate-fn. But, in the common cases where n is explicitly 8, 16, 32, or 64, it instead expands into a call of an optimized, inlined function.

Macro: signed-saturate

(defmacro signed-saturate (n x)
  (cond ((eql n 8)
         (cons 'signed-saturate8 (cons x 'nil)))
        ((eql n 16)
         (cons 'signed-saturate16 (cons x 'nil)))
        ((eql n 32)
         (cons 'signed-saturate32 (cons x 'nil)))
        ((eql n 64)
         (cons 'signed-saturate64 (cons x 'nil)))
        (t (cons 'signed-saturate-fn
                 (cons n (cons x 'nil))))))

Subtopics

Signed-saturate-fn
Logical definition of signed-saturate, and also its executable implementation in the general case.
Signed-saturate64
Optimized implementation of 64-bit signed saturation.
Signed-saturate32
Optimized implementation of 32-bit signed saturation.
Signed-saturate16
Optimized implementation of 16-bit signed saturation.
Signed-saturate8
Optimized implementation of 8-bit signed saturation.