Collect all instance names (not module names!) from a vl-modinstlist-p.
(vl-modinstlist->instnames x) → names
The Verilog-2005 Standard requires that module instances be named, but we relaxed that restriction in our definition of vl-modinst-p because of user-defined primitives, which may be unnamed. So, as with vl-gateinstlist->names, here we simply skip past any unnamed module instances.
Function:
(defun vl-modinstlist->instnames (x) (declare (xargs :guard (vl-modinstlist-p x))) (let ((__function__ 'vl-modinstlist->instnames)) (declare (ignorable __function__)) (mbe :logic (if (consp x) (if (vl-modinst->instname (car x)) (cons (vl-modinst->instname (car x)) (vl-modinstlist->instnames (cdr x))) (vl-modinstlist->instnames (cdr x))) nil) :exec (if (atom x) nil (with-local-nrev (vl-modinstlist->instnames-nrev x nrev))))))
Theorem:
(defthm string-listp-of-vl-modinstlist->instnames (b* ((names (vl-modinstlist->instnames x))) (string-listp names)) :rule-classes :rewrite)
Theorem:
(defthm vl-modinstlist->instnames-exec-removal (equal (vl-modinstlist->instnames-nrev x nrev) (append nrev (vl-modinstlist->instnames x))))
Theorem:
(defthm vl-modinstlist->instnames-when-not-consp (implies (not (consp x)) (equal (vl-modinstlist->instnames x) nil)))
Theorem:
(defthm vl-modinstlist->instnames-of-cons (equal (vl-modinstlist->instnames (cons a x)) (if (vl-modinst->instname a) (cons (vl-modinst->instname a) (vl-modinstlist->instnames x)) (vl-modinstlist->instnames x))))
Theorem:
(defthm vl-modinstlist->instnames-of-list-fix (equal (vl-modinstlist->instnames (list-fix x)) (vl-modinstlist->instnames x)))
Theorem:
(defthm vl-modinstlist->instnames-preserves-list-equiv (implies (list-equiv x x-equiv) (equal (vl-modinstlist->instnames x) (vl-modinstlist->instnames x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm vl-modinstlist->instnames-of-append (equal (vl-modinstlist->instnames (append x y)) (append (vl-modinstlist->instnames x) (vl-modinstlist->instnames y))))
Theorem:
(defthm vl-modinstlist->instnames-of-rev (equal (vl-modinstlist->instnames (rev x)) (rev (vl-modinstlist->instnames x))))
Theorem:
(defthm vl-modinstlist->instnames-of-vl-modinstlist-fix-x (equal (vl-modinstlist->instnames (vl-modinstlist-fix x)) (vl-modinstlist->instnames x)))
Theorem:
(defthm vl-modinstlist->instnames-vl-modinstlist-equiv-congruence-on-x (implies (vl-modinstlist-equiv x x-equiv) (equal (vl-modinstlist->instnames x) (vl-modinstlist->instnames x-equiv))) :rule-classes :congruence)