Generate a list of distinct wires with a particular range.
(vl-make-list-of-netdecls n basename range) → wires
Function:
(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:
(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:
(defthm len-of-vl-make-list-of-netdecls (equal (len (vl-make-list-of-netdecls n basename range)) (nfix n)))
Theorem:
(defthm consp-of-vl-make-list-of-netdecls (iff (vl-make-list-of-netdecls n basename range) (posp n)))
Theorem:
(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:
(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:
(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:
(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:
(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:
(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)