• Top

• Sv::vl-moddb.lisp

Vl-instarray-replicated-port-assigns

Signature

(vl-instarray-replicated-port-assigns 
     port-lhs instname conn-driver 
     instindex instoffset inst-incr) 
 
  → 
assigns

Arguments

port-lhs — Guard (sv::lhs-p port-lhs).

instname — Guard (stringp instname).

conn-driver — Guard (sv::driver-p conn-driver).

instindex — index of the current instance.
    Guard (integerp instindex).

instoffset — number of instances left.
    Guard (natp instoffset).

inst-incr — 1 or -1 depending on the direction of the range.
    Guard (integerp inst-incr).

Returns

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

Definitions and Theorems

Function: vl-instarray-replicated-port-assigns

(defun vl-instarray-replicated-port-assigns
       (port-lhs instname conn-driver
                 instindex instoffset inst-incr)
 (declare (xargs :guard (and (sv::lhs-p port-lhs)
                             (stringp instname)
                             (sv::driver-p conn-driver)
                             (integerp instindex)
                             (natp instoffset)
                             (integerp inst-incr))))
 (declare
  (xargs
       :guard
       (and (sv::svarlist-addr-p (sv::lhs-vars port-lhs))
            (sv::svarlist-addr-p
                 (sv::svex-vars (sv::driver->value conn-driver))))))
 (let ((__function__ 'vl-instarray-replicated-port-assigns))
   (declare (ignorable __function__))
   (b* (((when (zp instoffset)) nil)
        (instindex (lifix instindex))
        (lhs1 (sv::lhs-add-namespace
                   (string-fix instname)
                   (sv::lhs-add-namespace instindex port-lhs))))
     (cons (cons lhs1 (sv::driver-fix conn-driver))
           (vl-instarray-replicated-port-assigns
                port-lhs instname conn-driver
                (+ instindex (lifix inst-incr))
                (1- instoffset)
                inst-incr)))))

Theorem: assigns-p-of-vl-instarray-replicated-port-assigns

(defthm assigns-p-of-vl-instarray-replicated-port-assigns
  (b* ((assigns (vl-instarray-replicated-port-assigns
                     port-lhs instname conn-driver
                     instindex instoffset inst-incr)))
    (sv::assigns-p assigns))
  :rule-classes :rewrite)

Theorem: svarlist-addr-p-of-vl-instarray-replicated-port-assigns

(defthm svarlist-addr-p-of-vl-instarray-replicated-port-assigns
  (b* ((?assigns (vl-instarray-replicated-port-assigns
                      port-lhs instname conn-driver
                      instindex instoffset inst-incr)))
    (implies (sv::svarlist-addr-p
                  (sv::svex-vars (sv::driver->value conn-driver)))
             (sv::svarlist-addr-p (sv::assigns-vars assigns)))))

Theorem: vl-instarray-replicated-port-assigns-of-lhs-fix-port-lhs

(defthm vl-instarray-replicated-port-assigns-of-lhs-fix-port-lhs
  (equal (vl-instarray-replicated-port-assigns
              (sv::lhs-fix port-lhs)
              instname conn-driver
              instindex instoffset inst-incr)
         (vl-instarray-replicated-port-assigns
              port-lhs instname conn-driver
              instindex instoffset inst-incr)))

Theorem: vl-instarray-replicated-port-assigns-lhs-equiv-congruence-on-port-lhs

(defthm
 vl-instarray-replicated-port-assigns-lhs-equiv-congruence-on-port-lhs
 (implies (sv::lhs-equiv port-lhs port-lhs-equiv)
          (equal (vl-instarray-replicated-port-assigns
                      port-lhs instname conn-driver
                      instindex instoffset inst-incr)
                 (vl-instarray-replicated-port-assigns
                      port-lhs-equiv instname conn-driver
                      instindex instoffset inst-incr)))
 :rule-classes :congruence)

Theorem: vl-instarray-replicated-port-assigns-of-str-fix-instname

(defthm vl-instarray-replicated-port-assigns-of-str-fix-instname
  (equal (vl-instarray-replicated-port-assigns
              port-lhs (str-fix instname)
              conn-driver
              instindex instoffset inst-incr)
         (vl-instarray-replicated-port-assigns
              port-lhs instname conn-driver
              instindex instoffset inst-incr)))

Theorem: vl-instarray-replicated-port-assigns-streqv-congruence-on-instname

(defthm
 vl-instarray-replicated-port-assigns-streqv-congruence-on-instname
 (implies (streqv instname instname-equiv)
          (equal (vl-instarray-replicated-port-assigns
                      port-lhs instname conn-driver
                      instindex instoffset inst-incr)
                 (vl-instarray-replicated-port-assigns
                      port-lhs instname-equiv conn-driver
                      instindex instoffset inst-incr)))
 :rule-classes :congruence)

Theorem: vl-instarray-replicated-port-assigns-of-driver-fix-conn-driver

(defthm
     vl-instarray-replicated-port-assigns-of-driver-fix-conn-driver
  (equal (vl-instarray-replicated-port-assigns
              port-lhs
              instname (sv::driver-fix conn-driver)
              instindex instoffset inst-incr)
         (vl-instarray-replicated-port-assigns
              port-lhs instname conn-driver
              instindex instoffset inst-incr)))

Theorem: vl-instarray-replicated-port-assigns-driver-equiv-congruence-on-conn-driver

(defthm
 vl-instarray-replicated-port-assigns-driver-equiv-congruence-on-conn-driver
 (implies (sv::driver-equiv conn-driver conn-driver-equiv)
          (equal (vl-instarray-replicated-port-assigns
                      port-lhs instname conn-driver
                      instindex instoffset inst-incr)
                 (vl-instarray-replicated-port-assigns
                      port-lhs instname conn-driver-equiv
                      instindex instoffset inst-incr)))
 :rule-classes :congruence)

Theorem: vl-instarray-replicated-port-assigns-of-ifix-instindex

(defthm vl-instarray-replicated-port-assigns-of-ifix-instindex
  (equal (vl-instarray-replicated-port-assigns
              port-lhs
              instname conn-driver (ifix instindex)
              instoffset inst-incr)
         (vl-instarray-replicated-port-assigns
              port-lhs instname conn-driver
              instindex instoffset inst-incr)))

Theorem: vl-instarray-replicated-port-assigns-int-equiv-congruence-on-instindex

(defthm
 vl-instarray-replicated-port-assigns-int-equiv-congruence-on-instindex
 (implies (acl2::int-equiv instindex instindex-equiv)
          (equal (vl-instarray-replicated-port-assigns
                      port-lhs instname conn-driver
                      instindex instoffset inst-incr)
                 (vl-instarray-replicated-port-assigns
                      port-lhs instname conn-driver
                      instindex-equiv instoffset inst-incr)))
 :rule-classes :congruence)

Theorem: vl-instarray-replicated-port-assigns-of-nfix-instoffset

(defthm vl-instarray-replicated-port-assigns-of-nfix-instoffset
  (equal (vl-instarray-replicated-port-assigns
              port-lhs instname
              conn-driver instindex (nfix instoffset)
              inst-incr)
         (vl-instarray-replicated-port-assigns
              port-lhs instname conn-driver
              instindex instoffset inst-incr)))

Theorem: vl-instarray-replicated-port-assigns-nat-equiv-congruence-on-instoffset

(defthm
 vl-instarray-replicated-port-assigns-nat-equiv-congruence-on-instoffset
 (implies (acl2::nat-equiv instoffset instoffset-equiv)
          (equal (vl-instarray-replicated-port-assigns
                      port-lhs instname conn-driver
                      instindex instoffset inst-incr)
                 (vl-instarray-replicated-port-assigns
                      port-lhs instname conn-driver
                      instindex instoffset-equiv inst-incr)))
 :rule-classes :congruence)

Theorem: vl-instarray-replicated-port-assigns-of-ifix-inst-incr

(defthm vl-instarray-replicated-port-assigns-of-ifix-inst-incr
  (equal (vl-instarray-replicated-port-assigns
              port-lhs instname conn-driver
              instindex instoffset (ifix inst-incr))
         (vl-instarray-replicated-port-assigns
              port-lhs instname conn-driver
              instindex instoffset inst-incr)))

Theorem: vl-instarray-replicated-port-assigns-int-equiv-congruence-on-inst-incr

(defthm
 vl-instarray-replicated-port-assigns-int-equiv-congruence-on-inst-incr
 (implies (acl2::int-equiv inst-incr inst-incr-equiv)
          (equal (vl-instarray-replicated-port-assigns
                      port-lhs instname conn-driver
                      instindex instoffset inst-incr)
                 (vl-instarray-replicated-port-assigns
                      port-lhs instname conn-driver
                      instindex instoffset inst-incr-equiv)))
 :rule-classes :congruence)