(svex-gateinst-wirelist names) → wires
Function:
(defun svex-gateinst-wirelist (names) (declare (xargs :guard (string-listp names))) (let ((__function__ 'svex-gateinst-wirelist)) (declare (ignorable __function__)) (if (atom names) nil (cons (sv::make-wire :name (string-fix (car names)) :width 1 :low-idx 0 :revp nil) (svex-gateinst-wirelist (cdr names))))))
Theorem:
(defthm wirelist-p-of-svex-gateinst-wirelist (b* ((wires (svex-gateinst-wirelist names))) (sv::wirelist-p wires)) :rule-classes :rewrite)
Theorem:
(defthm svex-gateinst-wirelist-of-string-list-fix-names (equal (svex-gateinst-wirelist (string-list-fix names)) (svex-gateinst-wirelist names)))
Theorem:
(defthm svex-gateinst-wirelist-string-list-equiv-congruence-on-names (implies (str::string-list-equiv names names-equiv) (equal (svex-gateinst-wirelist names) (svex-gateinst-wirelist names-equiv))) :rule-classes :congruence)