• 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-design-use-set-report

Signature

(vl-design-use-set-report x omit) → (mv new-x report)

Arguments

x — Guard (vl-design-p x).

omit — Guard (string-listp omit).

Returns

new-x — Type (vl-design-p new-x).

report — Type (vl-useset-report-p report).

Definitions and Theorems

Function: vl-design-use-set-report

(defun vl-design-use-set-report (x omit)
  (declare (xargs :guard (and (vl-design-p x)
                              (string-listp omit))))
  (let ((__function__ 'vl-design-use-set-report))
    (declare (ignorable __function__))
    (b* ((x (vl-design-fix x))
         (omit (mbe :logic (if (string-listp omit) omit nil)
                    :exec omit))
         ((vl-design x) x)
         ((mv new-mods report)
          (vl-mark-wires-for-modulelist x.mods omit))
         (new-x (change-vl-design x :mods new-mods)))
      (mv new-x report))))

Theorem: vl-design-p-of-vl-design-use-set-report.new-x

(defthm vl-design-p-of-vl-design-use-set-report.new-x
  (b* (((mv ?new-x ?report)
        (vl-design-use-set-report x omit)))
    (vl-design-p new-x))
  :rule-classes :rewrite)

Theorem: vl-useset-report-p-of-vl-design-use-set-report.report

(defthm vl-useset-report-p-of-vl-design-use-set-report.report
  (b* (((mv ?new-x ?report)
        (vl-design-use-set-report x omit)))
    (vl-useset-report-p report))
  :rule-classes :rewrite)