• 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
            • Unsigned-saturate
              • Unsigned-saturate-fn
              • Unsigned-saturate8
              • Unsigned-saturate64
              • Unsigned-saturate32
              • Unsigned-saturate16
          • 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

Unsigned-saturate

(unsigned-saturate n x) coerces the integer x into an n-bit unsigned integer by unsigned saturation.

By unsigned saturation, we mean:

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

unsigned-saturate is actually a macro. Generally it expands into a call of unsigned-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: unsigned-saturate

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

Subtopics

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