Filter modules based on which of them have use-set problems.
(vl-split-useset-report x fine probs) → (mv fine probs)
Many modules do not have any unused or unset wires. Rather than verbosely include these in the report, we would like to throw them away and only keep the modules for which we have identified some problems.
This function walks over the report and accumulates into FINE the names of any modules for which we have nothing to report, and into PROBS the names of any modules for which we have something to report.
Function:
(defun vl-split-useset-report (x fine probs) (declare (xargs :guard (and (vl-useset-report-p x) (string-listp fine) (vl-useset-report-p probs)))) (let ((__function__ 'vl-split-useset-report)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv fine probs)) (entry (car x)) (name (vl-useset-report-entry->name entry)) (spurious (vl-useset-report-entry->spurious entry)) (unused (vl-useset-report-entry->unused entry)) (unset (vl-useset-report-entry->unset entry)) (warnings (vl-useset-report-entry->warnings entry)) (wwires (vl-useset-report-entry->wwires entry)) (lvalue-inputs (vl-useset-report-entry->lvalue-inputs entry)) (finep (and (null spurious) (null unused) (null unset) (null wwires) (null lvalue-inputs) (atom warnings)))) (vl-split-useset-report (cdr x) (if finep (cons name fine) fine) (if finep probs (cons entry probs))))))
Theorem:
(defthm string-listp-of-vl-split-useset-report.fine (implies (and (force (vl-useset-report-p x)) (force (string-listp fine)) (force (vl-useset-report-p probs))) (b* (((mv ?fine ?probs) (vl-split-useset-report x fine probs))) (string-listp fine))) :rule-classes :rewrite)
Theorem:
(defthm vl-useset-report-p-of-vl-split-useset-report.probs (implies (and (force (vl-useset-report-p x)) (force (string-listp fine)) (force (vl-useset-report-p probs))) (b* (((mv ?fine ?probs) (vl-split-useset-report x fine probs))) (vl-useset-report-p probs))) :rule-classes :rewrite)