• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Use-set

Vl-mark-wires-for-plainarg

Process a plain argument and mark its wires in the alist. If the direction of the argument hasn't been resolved, return the list of any wires that have been used, so that we can issue a warning about them.

Signature

(vl-mark-wires-for-plainarg x alist warning-wires) 
  → 
(mv new-alist warning-wires)

Arguments

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

alist — Guard (vl-wireinfo-alistp alist).

warning-wires — Guard (string-listp warning-wires).

Returns

new-alist — Type (vl-wireinfo-alistp new-alist), given the guard.

warning-wires — Type (string-listp warning-wires), given the guard.

Definitions and Theorems

Function: vl-mark-wires-for-plainarg

(defun vl-mark-wires-for-plainarg (x alist warning-wires)
 (declare (xargs :guard (and (vl-plainarg-p x)
                             (vl-wireinfo-alistp alist)
                             (string-listp warning-wires))))
 (let ((__function__ 'vl-mark-wires-for-plainarg))
  (declare (ignorable __function__))
  (b* ((expr (vl-plainarg->expr x))
       (dir (vl-plainarg->dir x))
       ((unless expr) (mv alist warning-wires))
       (wires (vl-expr-names expr)))
   (case
        dir
        (:vl-input (mv (vl-mark-wires-used wires t alist)
                       warning-wires))
        (:vl-output (mv (vl-mark-wires-set wires t alist)
                        warning-wires))
        (:vl-inout (let* ((alist (vl-mark-wires-used wires t alist))
                          (alist (vl-mark-wires-set wires t alist)))
                     (mv alist warning-wires)))
        (t (mv alist
               (revappend wires warning-wires)))))))

Theorem: vl-wireinfo-alistp-of-vl-mark-wires-for-plainarg.new-alist

(defthm vl-wireinfo-alistp-of-vl-mark-wires-for-plainarg.new-alist
 (implies (and (force (vl-plainarg-p x))
               (force (vl-wireinfo-alistp alist))
               (force (string-listp warning-wires)))
          (b* (((mv ?new-alist ?warning-wires)
                (vl-mark-wires-for-plainarg x alist warning-wires)))
            (vl-wireinfo-alistp new-alist)))
 :rule-classes :rewrite)

Theorem: string-listp-of-vl-mark-wires-for-plainarg.warning-wires

(defthm string-listp-of-vl-mark-wires-for-plainarg.warning-wires
 (implies (and (force (vl-plainarg-p x))
               (force (vl-wireinfo-alistp alist))
               (force (string-listp warning-wires)))
          (b* (((mv ?new-alist ?warning-wires)
                (vl-mark-wires-for-plainarg x alist warning-wires)))
            (string-listp warning-wires)))
 :rule-classes :rewrite)