Main function that performs the use-set analysis. We figure out which wires appear to be used and unused in the module X. We annotate the vardecls for the module with these attributes, and also generate a more concise vl-useset-report-entry object describing the status of this module.
(vl-mark-wires-for-module x omit) → (mv new-x report-entry)
Function:
(defun vl-mark-wires-for-module (x omit) (declare (xargs :guard (and (vl-module-p x) (string-listp omit)))) (let ((__function__ 'vl-mark-wires-for-module)) (declare (ignorable __function__)) (b* (((vl-module x) x) (warnings x.warnings) (declared-wires (vl-vardecllist->names-exec x.vardecls nil)) (params (vl-paramdecllist->names-exec x.paramdecls nil)) ((mv in out inout) (vl-portdecllist-names-by-direction x.portdecls nil nil nil)) (alist (vl-make-initial-wireinfo-alist (revappend params declared-wires))) (alist (vl-mark-wires-set omit nil alist)) (alist (vl-mark-wires-used omit nil alist)) (alist (vl-mark-wires-set params t alist)) (alist (vl-mark-wires-set in t alist)) (alist (vl-mark-wires-set inout t alist)) (alist (vl-mark-wires-used out t alist)) (alist (vl-mark-wires-used inout t alist)) (alist (vl-mark-wires-used (vl-exprlist-names (vl-portdecllist-allexprs x.portdecls)) t alist)) (alist (vl-mark-wires-used (vl-exprlist-names (vl-vardecllist-allexprs x.vardecls)) t alist)) (alist (vl-mark-wires-used (vl-exprlist-names (vl-paramdecllist-allexprs x.paramdecls)) t alist)) (warnings (if (and (atom x.alwayses) (atom x.initials)) (ok) (warn :type :vl-useset-statements-ignored :msg "Use-Set note: always and initial statements ~ are currently ignored in our wire analysis, so ~ use-set results may be incorrect."))) (alist (vl-mark-wires-for-assignlist x.assigns alist)) ((mv alist warnings warning-wires1) (vl-mark-wires-for-modinstlist x.modinsts alist warnings)) ((mv alist warnings warning-wires2) (vl-mark-wires-for-gateinstlist x.gateinsts alist warnings)) (warning-wires (vl-clean-up-warning-wires (mergesort (append warning-wires1 warning-wires2)) alist)) (- (fast-alist-free alist)) (alist (hons-shrink-alist alist nil)) ((mv unused unset) (vl-collect-unused-or-unset-wires alist nil nil)) (unused (mergesort unused)) (unset (mergesort unset)) (new-vardecls (if (or unused unset) (vl-annotate-vardecllist-with-wireinfo x.vardecls alist warning-wires) x.vardecls)) (x-prime (change-vl-module x :vardecls new-vardecls :warnings warnings)) ((mv implicit ?explicit) (vl-module-impexp-names x)) (implicit (mergesort implicit)) (bad (intersect implicit (union unused unset))) (good (difference (mergesort declared-wires) bad)) (typos (typo-detect bad good)) (spurious (intersect unused unset)) (unused (difference unused spurious)) (unset (difference unset spurious)) (report-entry (make-vl-useset-report-entry :name x.name :spurious spurious :unused unused :unset unset :wwires warning-wires :warnings warnings :typos typos))) (fast-alist-free alist) (mv x-prime report-entry))))
Theorem:
(defthm vl-module-p-of-vl-mark-wires-for-module.new-x (implies (vl-module-p x) (b* (((mv ?new-x ?report-entry) (vl-mark-wires-for-module x omit))) (vl-module-p new-x))) :rule-classes :rewrite)
Theorem:
(defthm vl-useset-report-entry-p-of-vl-mark-wires-for-module.report-entry (implies (and (force (vl-module-p x)) (force (string-listp omit))) (b* (((mv ?new-x ?report-entry) (vl-mark-wires-for-module x omit))) (vl-useset-report-entry-p report-entry))) :rule-classes :rewrite)