• 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
        • 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
  • Testing-utilities

• 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))))