• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
      • 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
            • Logcollapse
            • Limshift-loghead-of-logapp
            • Limshift-logext-of-logapp
            • Limshift-loghead-of-ash
          • Bitops/part-select
          • Bitops/parity
          • Bitops/saturate
          • Bitops/part-install
          • Bitops/logbitp-bounds
          • Bitops/ihsext-basics
          • Bitops/fast-rotate
          • Bitops/fast-logext
          • Bitops/ihs-extensions
        • Bv
        • Ihs
        • Rtl
      • Algebra
  • Bitops

Limited-shifts

Functions for performing shifts that are artificially limited so as to make them more amenable to symbolic execution with AIGs.

Subtopics

Logcollapse
OR together all the bits of x at position or above, collapsing them into the single bit at position.
Limshift-loghead-of-logapp
Computes (loghead full-width (logapp concat-width x y)).
Limshift-logext-of-logapp
Computes (loghead full-width (logapp concat-width x y)).
Limshift-loghead-of-ash
Computes (loghead width (ash x shift-amt)).