• Top

• Sv::vl-moddb.lisp

Vl-instarray-nonreplicated-port-lhs

Signature

(vl-instarray-nonreplicated-port-lhs 
     port-lhs 
     instname instindex instoffset inst-incr) 
 
  → 
scoped-lhs

Arguments

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

instname — Guard (stringp instname).

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

scoped-lhs — Type (sv::lhs-p scoped-lhs).

Definitions and Theorems

Function: vl-instarray-nonreplicated-port-lhs

(defun vl-instarray-nonreplicated-port-lhs
       (port-lhs instname instindex instoffset inst-incr)
  (declare (xargs :guard (and (sv::lhs-p port-lhs)
                              (stringp instname)
                              (integerp instindex)
                              (natp instoffset)
                              (integerp inst-incr))))
  (declare
       (xargs :guard (sv::svarlist-addr-p (sv::lhs-vars port-lhs))))
  (let ((__function__ 'vl-instarray-nonreplicated-port-lhs))
    (declare (ignorable __function__))
    (sv::lhs-add-namespace (string-fix instname)
                           (vl-instarray-nonreplicated-port-lhs-aux
                                port-lhs
                                instindex instoffset inst-incr))))

Theorem: lhs-p-of-vl-instarray-nonreplicated-port-lhs

(defthm lhs-p-of-vl-instarray-nonreplicated-port-lhs
  (b* ((scoped-lhs (vl-instarray-nonreplicated-port-lhs
                        port-lhs instname
                        instindex instoffset inst-incr)))
    (sv::lhs-p scoped-lhs))
  :rule-classes :rewrite)

Theorem: svarlist-addr-p-of-vl-instarray-nonreplicated-port-lhs

(defthm svarlist-addr-p-of-vl-instarray-nonreplicated-port-lhs
  (b* ((?scoped-lhs (vl-instarray-nonreplicated-port-lhs
                         port-lhs instname
                         instindex instoffset inst-incr)))
    (sv::svarlist-addr-p (sv::lhs-vars scoped-lhs))))

Theorem: vl-instarray-nonreplicated-port-lhs-of-lhs-fix-port-lhs

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

Theorem: vl-instarray-nonreplicated-port-lhs-lhs-equiv-congruence-on-port-lhs

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

Theorem: vl-instarray-nonreplicated-port-lhs-of-str-fix-instname

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

Theorem: vl-instarray-nonreplicated-port-lhs-streqv-congruence-on-instname

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

Theorem: vl-instarray-nonreplicated-port-lhs-of-ifix-instindex

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

Theorem: vl-instarray-nonreplicated-port-lhs-int-equiv-congruence-on-instindex

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

Theorem: vl-instarray-nonreplicated-port-lhs-of-nfix-instoffset

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

Theorem: vl-instarray-nonreplicated-port-lhs-nat-equiv-congruence-on-instoffset

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

Theorem: vl-instarray-nonreplicated-port-lhs-of-ifix-inst-incr

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

Theorem: vl-instarray-nonreplicated-port-lhs-int-equiv-congruence-on-inst-incr

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