		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-bit-index

Like logbit for 4vecs; the bit position must be a natp.

Signature
(4vec-bit-index n x) → bit
Arguments: n — The bit position to extract.
Guard (natp n).; x — The 4vec to extract it from.
Guard (4vec-p x).
Returns: bit — Type (4vec-p bit).

We extract the nth bit of x as a new 4vec.

We require that n is a natp instead of a 4vec, which makes this function suitable for modeling simple Verilog indexing expressions such as foo[3], but not for dynamic bit selects such as foo[i].

For a more general (but less efficient) function that drops this restriction and allows n to be a 4vec, see 4vec-bit-extract.

Definitions and Theorems

Function: 4vec-bit-index

(defun 4vec-bit-index (n x)
  (declare (xargs :guard (and (natp n) (4vec-p x))))
  (let ((__function__ '4vec-bit-index))
    (declare (ignorable __function__))
    (if-2vec-p
         (x)
         (2vec (logbit (lnfix n) (2vec->val x)))
         (make-4vec :upper (logbit (lnfix n) (4vec->upper x))
                    :lower (logbit (lnfix n) (4vec->lower x))))))

Theorem: 4vec-p-of-4vec-bit-index

(defthm 4vec-p-of-4vec-bit-index
  (b* ((bit (4vec-bit-index n x)))
    (4vec-p bit))
  :rule-classes :rewrite)

Theorem: 4vec-bit-index-of-nfix-n

(defthm 4vec-bit-index-of-nfix-n
  (equal (4vec-bit-index (nfix n) x)
         (4vec-bit-index n x)))

Theorem: 4vec-bit-index-nat-equiv-congruence-on-n

(defthm 4vec-bit-index-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (4vec-bit-index n x)
                  (4vec-bit-index n-equiv x)))
  :rule-classes :congruence)

Theorem: 4vec-bit-index-of-4vec-fix-x

(defthm 4vec-bit-index-of-4vec-fix-x
  (equal (4vec-bit-index n (4vec-fix x))
         (4vec-bit-index n x)))

Theorem: 4vec-bit-index-4vec-equiv-congruence-on-x

(defthm 4vec-bit-index-4vec-equiv-congruence-on-x
  (implies (4vec-equiv x x-equiv)
           (equal (4vec-bit-index n x)
                  (4vec-bit-index n x-equiv)))
  :rule-classes :congruence)