• 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
        • Bitops/part-select
        • Bitops/parity
        • Bitops/saturate
        • Bitops/part-install
          • Part-install
          • Part-select-and-part-install
        • Bitops/logbitp-bounds
        • Bitops/ihsext-basics
        • Bitops/fast-rotate
        • Bitops/fast-logext
        • Bitops/ihs-extensions
      • Bv
      • Ihs
      • Rtl
    • Algebra

• Bitops/part-install

Part-install

Set a portion of bits of an integer to some value

part-install is a macro that is defined in terms of the function part-install-width-low. This macro can be used to set a portion of bits from an integer to some value.

Usage:

(part-install val x :low 8 :high  15)   ;; x[15:8] = val
(part-install val x :low 8 :width  8)   ;; x[15:8] = val

Macro: part-install-width-low

(defmacro part-install-width-low (val x width low)
          (list 'part-install-width-low$inline
                val x width low))

Macro: part-install

(defmacro
 part-install (val x &key low high width)
 (cond
  ((and high width)
   (er hard? 'part-install
       "Can't use :high and :width together."))
  ((and low high (integerp low)
        (integerp high))
   (cons 'part-install-width-low
         (cons val
               (cons x
                     (cons (+ 1 high (- low))
                           (cons low 'nil))))))
  ((and low high)
   (cons
    'part-install-width-low
    (cons
     val
     (cons
      x
      (cons
          (cons '+
                (cons '1
                      (cons high
                            (cons (cons '- (cons low 'nil)) 'nil))))
          (cons low 'nil))))))
  ((and low width)
   (cons 'part-install-width-low
         (cons val
               (cons x (cons width (cons low 'nil))))))
  (t (er hard? 'part-install
         "Need either :low and :width, or :low and :high."))))

Definitions and Theorems

Function: part-install-width-low$inline

(defun part-install-width-low$inline
       (val x width low)
       (declare (xargs :guard (and (integerp x)
                                   (integerp val)
                                   (natp width)
                                   (natp low))))
       (mbe :logic (let* ((x (ifix x))
                          (val (ifix val))
                          (width (nfix width))
                          (low (nfix low))
                          (val (loghead width val))
                          (mask (logmask width)))
                         (logior (logand x (lognot (ash mask low)))
                                 (ash val low)))
            :exec (let* ((mask (1- (ash 1 width)))
                         (val (logand mask val)))
                        (logior (logand x (lognot (ash mask low)))
                                (ash val low)))))

Theorem: natp-part-install-width-low

(defthm natp-part-install-width-low
        (implies (<= 0 x)
                 (natp (part-install-width-low val x width low)))
        :rule-classes :type-prescription)

Theorem: int-equiv-implies-equal-part-install-width-low-1

(defthm
    int-equiv-implies-equal-part-install-width-low-1
    (implies (int-equiv val val-equiv)
             (equal (part-install-width-low val x width low)
                    (part-install-width-low val-equiv x width low)))
    :rule-classes (:congruence))

Theorem: int-equiv-implies-equal-part-install-width-low-2

(defthm
    int-equiv-implies-equal-part-install-width-low-2
    (implies (int-equiv x x-equiv)
             (equal (part-install-width-low val x width low)
                    (part-install-width-low val x-equiv width low)))
    :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-part-install-width-low-3

(defthm
    nat-equiv-implies-equal-part-install-width-low-3
    (implies (nat-equiv width width-equiv)
             (equal (part-install-width-low val x width low)
                    (part-install-width-low val x width-equiv low)))
    :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-part-install-width-low-4

(defthm
    nat-equiv-implies-equal-part-install-width-low-4
    (implies (nat-equiv low low-equiv)
             (equal (part-install-width-low val x width low)
                    (part-install-width-low val x width low-equiv)))
    :rule-classes (:congruence))

Theorem: unsigned-byte-p-=-n-of-part-install-width-low

(defthm
   unsigned-byte-p-=-n-of-part-install-width-low
   (implies
        (and (unsigned-byte-p n x)
             (<= (+ width low) n)
             (natp n)
             (natp low)
             (natp width))
        (unsigned-byte-p n
                         (part-install-width-low val x width low))))

Theorem: unsigned-byte-p->-n-of-part-install-width-low

(defthm
   unsigned-byte-p->-n-of-part-install-width-low
   (implies
        (and (unsigned-byte-p n x)
             (< n (+ width low))
             (natp low)
             (natp width))
        (unsigned-byte-p (+ low width)
                         (part-install-width-low val x width low))))