		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-concat

Like logapp for 4vecs; the width is also a 4vec.

Signature
(4vec-concat width low high) → concat
Arguments: width — Width of less-significant 4vec.
Guard (4vec-p width).; low — Source of the W less-significant bits.
Guard (4vec-p low).; high — Source of the rest of the bits.
Guard (4vec-p high).
Returns: concat — Type (4vec-p concat).

In the usual case, width is some natural number: we concatenate the width least significant bits of low with all of high. That is, we produce a new 4vec which might be written in Verilog as {high, low[width-1:0]}.

Since width is a 4vec it may have X or Z bits or may be negative. In this case, the result is infinite Xes.

Definitions and Theorems

Function: 4vec-concat

(defun 4vec-concat (width low high)
 (declare (xargs :guard (and (4vec-p width)
                             (4vec-p low)
                             (4vec-p high))))
 (let ((__function__ '4vec-concat))
   (declare (ignorable __function__))
   (if
    (and (2vec-p width)
         (<= 0 (2vec->val width)))
    (if
     (mbe :logic nil
          :exec
          (and (>= (2vec->val width) (4vec-bit-limit))
               (b* (((4vec low)) ((4vec high)))
                 (or (if (< low.upper 0)
                         (not (eql high.upper -1))
                       (not (eql high.upper 0)))
                     (if (< low.lower 0)
                         (not (eql high.lower -1))
                       (not (eql high.lower 0)))))
               (4vec-very-large-integer-warning (2vec->val width))))
     (4vec-x)
     (b* ((wval (2vec->val width)))
       (if-2vec-p (low high)
                  (2vec (logapp wval (2vec->val low)
                                (2vec->val high)))
                  (b* (((4vec low)) ((4vec high)))
                    (4vec (logapp wval low.upper high.upper)
                          (logapp wval low.lower high.lower))))))
    (4vec-x))))

Theorem: 4vec-p-of-4vec-concat

(defthm 4vec-p-of-4vec-concat
  (b* ((concat (4vec-concat width low high)))
    (4vec-p concat))
  :rule-classes :rewrite)

Theorem: 4vec-concat-of-2vecnatx-fix-width

(defthm 4vec-concat-of-2vecnatx-fix-width
  (equal (4vec-concat (2vecnatx-fix width)
                      low high)
         (4vec-concat width low high)))

Theorem: 4vec-concat-2vecnatx-equiv-congruence-on-width

(defthm 4vec-concat-2vecnatx-equiv-congruence-on-width
  (implies (2vecnatx-equiv width width-equiv)
           (equal (4vec-concat width low high)
                  (4vec-concat width-equiv low high)))
  :rule-classes :congruence)

Theorem: 4vec-concat-of-4vec-fix-low

(defthm 4vec-concat-of-4vec-fix-low
  (equal (4vec-concat width (4vec-fix low) high)
         (4vec-concat width low high)))

Theorem: 4vec-concat-4vec-equiv-congruence-on-low

(defthm 4vec-concat-4vec-equiv-congruence-on-low
  (implies (4vec-equiv low low-equiv)
           (equal (4vec-concat width low high)
                  (4vec-concat width low-equiv high)))
  :rule-classes :congruence)

Theorem: 4vec-concat-of-4vec-fix-high

(defthm 4vec-concat-of-4vec-fix-high
  (equal (4vec-concat width low (4vec-fix high))
         (4vec-concat width low high)))

Theorem: 4vec-concat-4vec-equiv-congruence-on-high

(defthm 4vec-concat-4vec-equiv-congruence-on-high
  (implies (4vec-equiv high high-equiv)
           (equal (4vec-concat width low high)
                  (4vec-concat width low high-equiv)))
  :rule-classes :congruence)