• Top

• Sv::vl-moddb.lisp

Vl-portinfo-vars

Signature

(vl-portinfo-vars x) → vars

Arguments

x — Guard (vl-portinfo-p x).

Returns

vars — Type (sv::svarlist-p vars).

Definitions and Theorems

Function: vl-portinfo-vars

(defun vl-portinfo-vars (x)
  (declare (xargs :guard (vl-portinfo-p x)))
  (let ((__function__ 'vl-portinfo-vars))
    (declare (ignorable __function__))
    (vl-portinfo-case x
                      :regular (append (sv::lhs-vars x.port-lhs)
                                       (sv::svex-vars x.conn-svex))
                      :otherwise nil)))

Theorem: svarlist-p-of-vl-portinfo-vars

(defthm svarlist-p-of-vl-portinfo-vars
  (b* ((vars (vl-portinfo-vars x)))
    (sv::svarlist-p vars))
  :rule-classes :rewrite)

Theorem: svarlist-addr-p-of-vl-portinfo-vars-implies

(defthm svarlist-addr-p-of-vl-portinfo-vars-implies
 (implies
  (sv::svarlist-addr-p (vl-portinfo-vars x))
  (and
   (implies
      (vl-portinfo-case x :regular)
      (b* (((vl-portinfo-regular x)))
        (and (sv::svarlist-addr-p (sv::lhs-vars x.port-lhs))
             (sv::svarlist-addr-p (sv::svex-vars x.conn-svex))))))))

Theorem: true-listp-of-vl-portinfo-vars

(defthm true-listp-of-vl-portinfo-vars
  (b* ((?vars (vl-portinfo-vars x)))
    (true-listp vars))
  :rule-classes :type-prescription)

Theorem: vl-portinfo-vars-of-vl-portinfo-fix-x

(defthm vl-portinfo-vars-of-vl-portinfo-fix-x
  (equal (vl-portinfo-vars (vl-portinfo-fix x))
         (vl-portinfo-vars x)))

Theorem: vl-portinfo-vars-vl-portinfo-equiv-congruence-on-x

(defthm vl-portinfo-vars-vl-portinfo-equiv-congruence-on-x
  (implies (vl-portinfo-equiv x x-equiv)
           (equal (vl-portinfo-vars x)
                  (vl-portinfo-vars x-equiv)))
  :rule-classes :congruence)