Carry out use-set analysis on all modules.
(vl-mark-wires-for-modulelist x omit) → (mv new-x report)
Function:
(defun vl-mark-wires-for-modulelist (x omit) (declare (xargs :guard (and (vl-modulelist-p x) (string-listp omit)))) (let ((__function__ 'vl-mark-wires-for-modulelist)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil)) ((mv car-prime car-entry) (vl-mark-wires-for-module (car x) omit)) ((mv cdr-prime cdr-report) (vl-mark-wires-for-modulelist (cdr x) omit))) (mv (cons car-prime cdr-prime) (cons car-entry cdr-report)))))
Theorem:
(defthm vl-modulelist-p-of-vl-mark-wires-for-modulelist.new-x (implies (vl-modulelist-p x) (b* (((mv ?new-x ?report) (vl-mark-wires-for-modulelist x omit))) (vl-modulelist-p new-x))) :rule-classes :rewrite)
Theorem:
(defthm vl-useset-report-p-of-vl-mark-wires-for-modulelist.report (implies (and (vl-modulelist-p x) (string-listp omit)) (b* (((mv ?new-x ?report) (vl-mark-wires-for-modulelist x omit))) (vl-useset-report-p report))) :rule-classes :rewrite)