		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

4vec-extend

Returns an 4vec representing the sign- or zero-extension of x at the given width.

Signature
(4vec-extend type width x) → sv
Arguments: type — Guard (vl-exprsign-p type).; width — Guard (natp width).; x — Guard (sv::4vec-p x).
Returns: sv — Type (sv::4vec-p sv).

We don't have to extend/truncate operands when translating VL expressions like a & b, but we do need to do it to the inputs of expressions like a < b, to chop off any garbage in the upper bits.

Definitions and Theorems

Function: 4vec-extend

(defun 4vec-extend (type width x)
  (declare (xargs :guard (and (vl-exprsign-p type)
                              (natp width)
                              (sv::4vec-p x))))
  (let ((__function__ '4vec-extend))
    (declare (ignorable __function__))
    (if (vl-exprsign-equiv type :vl-signed)
        (sv::4vec-sign-ext (sv::2vec (lnfix width))
                           x)
      (sv::4vec-zero-ext (sv::2vec (lnfix width))
                         x))))

Theorem: 4vec-p-of-4vec-extend

(defthm 4vec-p-of-4vec-extend
  (b* ((sv (4vec-extend type width x)))
    (sv::4vec-p sv))
  :rule-classes :rewrite)

Theorem: 4vec-extend-of-vl-exprsign-fix-type

(defthm 4vec-extend-of-vl-exprsign-fix-type
  (equal (4vec-extend (vl-exprsign-fix type)
                      width x)
         (4vec-extend type width x)))

Theorem: 4vec-extend-vl-exprsign-equiv-congruence-on-type

(defthm 4vec-extend-vl-exprsign-equiv-congruence-on-type
  (implies (vl-exprsign-equiv type type-equiv)
           (equal (4vec-extend type width x)
                  (4vec-extend type-equiv width x)))
  :rule-classes :congruence)

Theorem: 4vec-extend-of-nfix-width

(defthm 4vec-extend-of-nfix-width
  (equal (4vec-extend type (nfix width) x)
         (4vec-extend type width x)))

Theorem: 4vec-extend-nat-equiv-congruence-on-width

(defthm 4vec-extend-nat-equiv-congruence-on-width
  (implies (acl2::nat-equiv width width-equiv)
           (equal (4vec-extend type width x)
                  (4vec-extend type width-equiv x)))
  :rule-classes :congruence)

Theorem: 4vec-extend-of-4vec-fix-x

(defthm 4vec-extend-of-4vec-fix-x
  (equal (4vec-extend type width (sv::4vec-fix x))
         (4vec-extend type width x)))

Theorem: 4vec-extend-4vec-equiv-congruence-on-x

(defthm 4vec-extend-4vec-equiv-congruence-on-x
  (implies (sv::4vec-equiv x x-equiv)
           (equal (4vec-extend type width x)
                  (4vec-extend type width x-equiv)))
  :rule-classes :congruence)