		Search-engine friendly clone of the ACL2 documentation.

Use-set

Vl-mark-wires-for-modulelist

Carry out use-set analysis on all modules.

Signature
(vl-mark-wires-for-modulelist x omit) → (mv new-x report)
Arguments: x — Modules to analyze.
Guard (vl-modulelist-p x).; omit — Special wires not to report as unused/unset.
Guard (string-listp omit).
Returns: new-x — Updated modules, where perhaps some wires have been annotated with attributes like VL_UNUSED.
Type (vl-modulelist-p new-x), given (vl-modulelist-p x).; report — Report about unused/unset wires for all modules.
Type (vl-useset-report-p report), given the guard.

Definitions and Theorems

Function: vl-mark-wires-for-modulelist

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

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

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