• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
        • Typo-detection
        • Vl-wireinfo-alistp
        • Vl-annotate-vardecllist-with-wireinfo
        • Vl-useset-report-entry-p
        • Vl-print-useset-report-entry
        • Vl-mark-wires-for-module
        • Vl-split-useset-report
        • Vl-annotate-vardecl-with-wireinfo
        • Vl-mark-wires-for-modinstlist
        • Vl-mark-wires-for-modinst
        • Vl-mark-wires-for-gateinstlist
        • Vl-mark-wires-for-gateinst
        • Vl-mark-wires-for-plainarg
        • Vl-wireinfo-p
        • Vl-mark-wires-for-modulelist
        • Vl-vardecllist-impexp-names
        • Vl-report-totals
        • Vl-mark-wires-for-plainarglist
        • Vl-collect-unused-or-unset-wires
        • Vl-clean-up-warning-wires
        • Vl-print-useset-report-top
        • Vl-mark-wires-for-arguments
        • Vl-useset-report-p
        • Vl-star-names-of-warning-wires
        • Vl-design-use-set-report
        • Vl-module-impexp-names
        • Vl-make-initial-wireinfo-alist
        • Vl-mark-wire-used
        • Vl-mark-wire-set
        • Vl-mark-wires-used
        • Vl-mark-wires-for-assignment
        • Vl-mark-wires-for-assignlist
        • Vl-mark-wires-set
        • Vl-print-useset-report-full-aux
        • Vl-print-typo-alist
        • Vl-print-typo-possibilities
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • Svl
    • X86isa
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Use-set

Vl-split-useset-report

Filter modules based on which of them have use-set problems.

Signature

(vl-split-useset-report x fine probs) → (mv fine probs)

Arguments

x — Guard (vl-useset-report-p x).

fine — Guard (string-listp fine).

probs — Guard (vl-useset-report-p probs).

Returns

fine — Names of modules with no problems.
    Type (string-listp fine), given the guard.

probs — Subset of X that actually has problems.
    Type (vl-useset-report-p probs), given the guard.

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.

Definitions and Theorems

Function: vl-split-useset-report

(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: string-listp-of-vl-split-useset-report.fine

(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: vl-useset-report-p-of-vl-split-useset-report.probs

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