		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Svex-extend

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

Signature
(svex-extend type width x) → sv
Arguments: type — Guard (vl-exprsign-p type).; width — Guard (natp width).; x — Guard (sv::svex-p x).
Returns: sv — Type (sv::svex-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: svex-extend

(defun svex-extend (type width x)
  (declare (xargs :guard (and (vl-exprsign-p type)
                              (natp width)
                              (sv::svex-p x))))
  (let ((__function__ 'svex-extend))
    (declare (ignorable __function__))
    (if (vl-exprsign-equiv type :vl-signed)
        (sv::svex-signx width x)
      (sv::svex-zerox width x))))

Theorem: svex-p-of-svex-extend

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

Theorem: svex-vars-of-svex-extend

(defthm svex-vars-of-svex-extend
  (implies
       (not (member v (sv::svex-vars x)))
       (not (member v
                    (sv::svex-vars (svex-extend type width x))))))

Theorem: svex-extend-of-vl-exprsign-fix-type

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

Theorem: svex-extend-vl-exprsign-equiv-congruence-on-type

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

Theorem: svex-extend-of-nfix-width

(defthm svex-extend-of-nfix-width
  (equal (svex-extend type (nfix width) x)
         (svex-extend type width x)))

Theorem: svex-extend-nat-equiv-congruence-on-width

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

Theorem: svex-extend-of-svex-fix-x

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

Theorem: svex-extend-svex-equiv-congruence-on-x

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