• Top

• Sv::vl-moddb.lisp

Vl-instarray-nonreplicated-port-lhs-aux

Signature

(vl-instarray-nonreplicated-port-lhs-aux 
     port-lhs instindex instoffset inst-incr) 
 
  → 
array-lhs

Arguments

port-lhs — Guard (sv::lhs-p port-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

array-lhs — Port-lhs appended instoffset times scoped by the various instindices.
    Type (sv::lhs-p array-lhs).

Definitions and Theorems

Function: vl-instarray-nonreplicated-port-lhs-aux

(defun vl-instarray-nonreplicated-port-lhs-aux
       (port-lhs instindex instoffset inst-incr)
  (declare (xargs :guard (and (sv::lhs-p port-lhs)
                              (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-aux))
    (declare (ignorable __function__))
    (b* (((when (zp instoffset)) nil)
         (instindex (lifix instindex))
         (lhs1 (sv::lhs-add-namespace instindex port-lhs)))
      (append-without-guard
           lhs1
           (vl-instarray-nonreplicated-port-lhs-aux
                port-lhs (+ instindex (lifix inst-incr))
                (1- instoffset)
                inst-incr)))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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