• Top

• Sv::vl-moddb.lisp

Vl-instarray-replicated-port-aliases

Signature

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

Arguments

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

instname — Guard (stringp instname).

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

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

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

Definitions and Theorems

Function: vl-instarray-replicated-port-aliases

(defun vl-instarray-replicated-port-aliases
       (port-lhs instname
                 conn-lhs instindex instoffset inst-incr)
 (declare (xargs :guard (and (sv::lhs-p port-lhs)
                             (stringp instname)
                             (sv::lhs-p conn-lhs)
                             (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::lhs-vars conn-lhs)))))
 (let ((__function__ 'vl-instarray-replicated-port-aliases))
   (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 (sv::lhs-fix conn-lhs) lhs1)
           (vl-instarray-replicated-port-aliases
                port-lhs instname
                conn-lhs (+ instindex (lifix inst-incr))
                (1- instoffset)
                inst-incr)))))

Theorem: lhspairs-p-of-vl-instarray-replicated-port-aliases

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

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

(defthm svarlist-addr-p-of-vl-instarray-replicated-port-aliases
  (b* ((?aliases (vl-instarray-replicated-port-aliases
                      port-lhs instname conn-lhs
                      instindex instoffset inst-incr)))
    (implies (sv::svarlist-addr-p (sv::lhs-vars conn-lhs))
             (sv::svarlist-addr-p (sv::lhspairs-vars aliases)))))

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

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

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

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

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

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

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

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

Theorem: vl-instarray-replicated-port-aliases-of-lhs-fix-conn-lhs

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

Theorem: vl-instarray-replicated-port-aliases-lhs-equiv-congruence-on-conn-lhs

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

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

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

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

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

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

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

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

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

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

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

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

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