Gather names of unused/unset wires from a wireinfo alist.
(vl-collect-unused-or-unset-wires x unused unset) → (mv unused unset)
Function:
(defun vl-collect-unused-or-unset-wires (x unused unset) (declare (xargs :guard (and (vl-wireinfo-alistp x) (string-listp unused) (string-listp unset)))) (let ((__function__ 'vl-collect-unused-or-unset-wires)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv unused unset)) (name (caar x)) (info (cdar x)) (usedp (vl-wireinfo->usedp info)) (setp (vl-wireinfo->setp info))) (vl-collect-unused-or-unset-wires (cdr x) (if usedp unused (cons name unused)) (if setp unset (cons name unset))))))
Theorem:
(defthm string-listp-of-vl-collect-unused-or-unset-wires.unused (implies (and (force (vl-wireinfo-alistp x)) (force (string-listp unused)) (force (string-listp unset))) (b* (((mv ?unused ?unset) (vl-collect-unused-or-unset-wires x unused unset))) (string-listp unused))) :rule-classes :rewrite)
Theorem:
(defthm string-listp-of-vl-collect-unused-or-unset-wires.unset (implies (and (force (vl-wireinfo-alistp x)) (force (string-listp unused)) (force (string-listp unset))) (b* (((mv ?unused ?unset) (vl-collect-unused-or-unset-wires x unused unset))) (string-listp unset))) :rule-classes :rewrite)