• Top

• Sv::vl-moddb.lisp

Vl-portinfolist-to-svex-assigns/aliases

Signature

(vl-portinfolist-to-svex-assigns/aliases x instname range) 
  → 
(mv warnings assigns aliases)

Arguments

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

instname — Guard (stringp instname).

range — Guard (vl-maybe-range-p range).

Returns

warnings — Type (vl-warninglist-p warnings).

assigns — Type (sv::assigns-p assigns).

aliases — Type (sv::lhspairs-p aliases).

Definitions and Theorems

Function: vl-portinfolist-to-svex-assigns/aliases

(defun vl-portinfolist-to-svex-assigns/aliases (x instname range)
 (declare (xargs :guard (and (vl-portinfolist-p x)
                             (stringp instname)
                             (vl-maybe-range-p range))))
 (declare
   (xargs :guard (and (sv::svarlist-addr-p (vl-portinfolist-vars x))
                      (vl-maybe-range-resolved-p range))))
 (let ((__function__ 'vl-portinfolist-to-svex-assigns/aliases))
   (declare (ignorable __function__))
   (b* ((warnings nil)
        ((when (atom x)) (mv (ok) nil nil))
        ((wmv warnings assigns1 aliases1)
         (vl-portinfo-to-svex-assign-or-alias (car x)
                                              instname range))
        ((wmv warnings assigns2 aliases2)
         (vl-portinfolist-to-svex-assigns/aliases (cdr x)
                                                  instname range)))
     (mv warnings (append assigns1 assigns2)
         (append aliases1 aliases2)))))

Theorem: vl-warninglist-p-of-vl-portinfolist-to-svex-assigns/aliases.warnings

(defthm
 vl-warninglist-p-of-vl-portinfolist-to-svex-assigns/aliases.warnings
 (b* (((mv ?warnings ?assigns ?aliases)
       (vl-portinfolist-to-svex-assigns/aliases x instname range)))
   (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: assigns-p-of-vl-portinfolist-to-svex-assigns/aliases.assigns

(defthm assigns-p-of-vl-portinfolist-to-svex-assigns/aliases.assigns
  (b* (((mv ?warnings ?assigns ?aliases)
        (vl-portinfolist-to-svex-assigns/aliases x instname range)))
    (sv::assigns-p assigns))
  :rule-classes :rewrite)

Theorem: lhspairs-p-of-vl-portinfolist-to-svex-assigns/aliases.aliases

(defthm
      lhspairs-p-of-vl-portinfolist-to-svex-assigns/aliases.aliases
  (b* (((mv ?warnings ?assigns ?aliases)
        (vl-portinfolist-to-svex-assigns/aliases x instname range)))
    (sv::lhspairs-p aliases))
  :rule-classes :rewrite)

Theorem: var-of-vl-portinfolist-to-svex-assigns/aliases

(defthm var-of-vl-portinfolist-to-svex-assigns/aliases
  (b* (((mv ?warnings ?assigns ?aliases)
        (vl-portinfolist-to-svex-assigns/aliases x instname range)))
    (implies
         (sv::svarlist-addr-p (vl-portinfolist-vars x))
         (and (sv::svarlist-addr-p (sv::assigns-vars assigns))
              (sv::svarlist-addr-p (sv::lhspairs-vars aliases))))))

Theorem: vl-portinfolist-to-svex-assigns/aliases-mvtypes-1

(defthm vl-portinfolist-to-svex-assigns/aliases-mvtypes-1
 (true-listp
   (mv-nth
        1
        (vl-portinfolist-to-svex-assigns/aliases x instname range)))
 :rule-classes :type-prescription)

Theorem: vl-portinfolist-to-svex-assigns/aliases-mvtypes-2

(defthm vl-portinfolist-to-svex-assigns/aliases-mvtypes-2
 (true-listp
   (mv-nth
        2
        (vl-portinfolist-to-svex-assigns/aliases x instname range)))
 :rule-classes :type-prescription)

Theorem: vl-portinfolist-to-svex-assigns/aliases-of-vl-portinfolist-fix-x

(defthm
   vl-portinfolist-to-svex-assigns/aliases-of-vl-portinfolist-fix-x
 (equal
    (vl-portinfolist-to-svex-assigns/aliases (vl-portinfolist-fix x)
                                             instname range)
    (vl-portinfolist-to-svex-assigns/aliases x instname range)))

Theorem: vl-portinfolist-to-svex-assigns/aliases-vl-portinfolist-equiv-congruence-on-x

(defthm
 vl-portinfolist-to-svex-assigns/aliases-vl-portinfolist-equiv-congruence-on-x
 (implies
   (vl-portinfolist-equiv x x-equiv)
   (equal (vl-portinfolist-to-svex-assigns/aliases x instname range)
          (vl-portinfolist-to-svex-assigns/aliases
               x-equiv instname range)))
 :rule-classes :congruence)

Theorem: vl-portinfolist-to-svex-assigns/aliases-of-str-fix-instname

(defthm vl-portinfolist-to-svex-assigns/aliases-of-str-fix-instname
  (equal
       (vl-portinfolist-to-svex-assigns/aliases x (str-fix instname)
                                                range)
       (vl-portinfolist-to-svex-assigns/aliases x instname range)))

Theorem: vl-portinfolist-to-svex-assigns/aliases-streqv-congruence-on-instname

(defthm
 vl-portinfolist-to-svex-assigns/aliases-streqv-congruence-on-instname
 (implies
   (streqv instname instname-equiv)
   (equal (vl-portinfolist-to-svex-assigns/aliases x instname range)
          (vl-portinfolist-to-svex-assigns/aliases
               x instname-equiv range)))
 :rule-classes :congruence)

Theorem: vl-portinfolist-to-svex-assigns/aliases-of-vl-maybe-range-fix-range

(defthm
 vl-portinfolist-to-svex-assigns/aliases-of-vl-maybe-range-fix-range
 (equal (vl-portinfolist-to-svex-assigns/aliases
             x instname (vl-maybe-range-fix range))
        (vl-portinfolist-to-svex-assigns/aliases x instname range)))

Theorem: vl-portinfolist-to-svex-assigns/aliases-vl-maybe-range-equiv-congruence-on-range

(defthm
 vl-portinfolist-to-svex-assigns/aliases-vl-maybe-range-equiv-congruence-on-range
 (implies
   (vl-maybe-range-equiv range range-equiv)
   (equal (vl-portinfolist-to-svex-assigns/aliases x instname range)
          (vl-portinfolist-to-svex-assigns/aliases
               x instname range-equiv)))
 :rule-classes :congruence)