		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-list-of-netdecls

Generate a list of distinct wires with a particular range.

Signature
(vl-make-list-of-netdecls n basename range) → wires
Arguments: n — how many wires to generate.
Guard (natp n).; basename — generate wires like basename_3.
Guard (stringp basename).; range — range for each generated wire.
Guard (vl-maybe-range-p range).
Returns: wires — Type (vl-vardecllist-p wires).

Definitions and Theorems

Function: vl-make-list-of-netdecls

(defun vl-make-list-of-netdecls (n basename range)
 (declare (xargs :guard (and (natp n)
                             (stringp basename)
                             (vl-maybe-range-p range))))
 (let ((__function__ 'vl-make-list-of-netdecls))
  (declare (ignorable __function__))
  (b*
   (((when (zp n)) nil)
    (range (vl-maybe-range-fix range))
    (type
     (hons-copy (make-vl-coretype :name :vl-logic
                                  :pdims (and range (list range)))))
    (decl1 (make-vl-vardecl :name (cat basename "_" (natstr n))
                            :type type
                            :nettype :vl-wire
                            :loc *vl-fakeloc*)))
   (cons decl1
         (vl-make-list-of-netdecls (- n 1)
                                   basename range)))))

Theorem: vl-vardecllist-p-of-vl-make-list-of-netdecls

(defthm vl-vardecllist-p-of-vl-make-list-of-netdecls
  (b* ((wires (vl-make-list-of-netdecls n basename range)))
    (vl-vardecllist-p wires))
  :rule-classes :rewrite)

Theorem: len-of-vl-make-list-of-netdecls

(defthm len-of-vl-make-list-of-netdecls
  (equal (len (vl-make-list-of-netdecls n basename range))
         (nfix n)))

Theorem: consp-of-vl-make-list-of-netdecls

(defthm consp-of-vl-make-list-of-netdecls
  (iff (vl-make-list-of-netdecls n basename range)
       (posp n)))

Theorem: vl-make-list-of-netdecls-of-nfix-n

(defthm vl-make-list-of-netdecls-of-nfix-n
  (equal (vl-make-list-of-netdecls (nfix n)
                                   basename range)
         (vl-make-list-of-netdecls n basename range)))

Theorem: vl-make-list-of-netdecls-nat-equiv-congruence-on-n

(defthm vl-make-list-of-netdecls-nat-equiv-congruence-on-n
 (implies (acl2::nat-equiv n n-equiv)
          (equal (vl-make-list-of-netdecls n basename range)
                 (vl-make-list-of-netdecls n-equiv basename range)))
 :rule-classes :congruence)

Theorem: vl-make-list-of-netdecls-of-str-fix-basename

(defthm vl-make-list-of-netdecls-of-str-fix-basename
  (equal (vl-make-list-of-netdecls n (str-fix basename)
                                   range)
         (vl-make-list-of-netdecls n basename range)))

Theorem: vl-make-list-of-netdecls-streqv-congruence-on-basename

(defthm vl-make-list-of-netdecls-streqv-congruence-on-basename
 (implies (streqv basename basename-equiv)
          (equal (vl-make-list-of-netdecls n basename range)
                 (vl-make-list-of-netdecls n basename-equiv range)))
 :rule-classes :congruence)

Theorem: vl-make-list-of-netdecls-of-vl-maybe-range-fix-range

(defthm vl-make-list-of-netdecls-of-vl-maybe-range-fix-range
 (equal
    (vl-make-list-of-netdecls n basename (vl-maybe-range-fix range))
    (vl-make-list-of-netdecls n basename range)))

Theorem: vl-make-list-of-netdecls-vl-maybe-range-equiv-congruence-on-range

(defthm
  vl-make-list-of-netdecls-vl-maybe-range-equiv-congruence-on-range
 (implies (vl-maybe-range-equiv range range-equiv)
          (equal (vl-make-list-of-netdecls n basename range)
                 (vl-make-list-of-netdecls n basename range-equiv)))
 :rule-classes :congruence)