		Search-engine friendly clone of the ACL2 documentation.

Use-set

Vl-mark-wires-for-module

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.

Signature
(vl-mark-wires-for-module x omit) → (mv new-x report-entry)
Arguments: x — Module to analyze.
Guard (vl-module-p x).; omit — Names of any special wires to omit,.
Guard (string-listp omit).
Returns: new-x — Type (vl-module-p new-x), given (vl-module-p x).; report-entry — Type (vl-useset-report-entry-p report-entry), given the guard.

Definitions and Theorems

Function: vl-mark-wires-for-module

(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: vl-module-p-of-vl-mark-wires-for-module.new-x

(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: vl-useset-report-entry-p-of-vl-mark-wires-for-module.report-entry

(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)