• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
        • Unparameterization
        • Elaborate
        • Addnames
        • Annotate
          • Increment-elim
          • Make-implicit-wires
          • Basic-bind-elim
          • Argresolve
            • Vl-convert-namedargs
              • Vl-expand-dotstar-arguments
              • Vl-convert-namedargs-aux
              • Vl-find-namedarg
              • Vl-convert-namedargs-aux-fal
            • Vl-unhierarchicalize-interfaceport
            • Vl-interfacelist-argresolve
            • Vl-modulelist-argresolve
            • Vl-gateinst-dirassign
            • Vl-arguments-argresolve
            • Vl-unhierarchicalize-interfaceports
            • Vl-check-blankargs
            • Vl-annotate-plainargs
            • Vl-modinst-maybe-argresolve
            • Vl-modinst-argresolve
            • Vl-modinstlist-argresolve
            • Vl-gateinstlist-dirassign
            • Vl-interface-argresolve
            • Vl-module-argresolve
            • Vl-namedarglist-alist
            • Vl-make-namedarg-alist
            • Vl-design-argresolve
            • Vl-fast-find-namedarg
            • Vl-namedarg-alist
            • Vl-scopeitem-modport-p
            • Vl-scopeitem-modinst-p
            • Vl-scopeitem-interfaceport-p
            • Vl-port-interface-p
          • Basicsanity
          • Portdecl-sign
          • Enum-names
          • Port-resolve
          • Udp-elim
          • Vl-annotate-design
          • Vl-annotate-module
        • Clean-warnings
        • Eliminitial
        • Custom-transform-hooks
        • Problem-modules
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-convert-namedargs

Vl-find-namedarg

Look up an argument by name in a named argument list.

Signature

(vl-find-namedarg name args) → *

Arguments

name — Guard (stringp name).

args — Guard (vl-namedarglist-p args).

We once used some fast-alist stuff here, but now I think that it isn't worthwhile since most module instances either have relatively few arguments or are instantiated infrequently. It'd be easy enough to write an version that uses fast-alists when there are many arguments if performance becomes a problem.

Definitions and Theorems

Function: vl-find-namedarg

(defun vl-find-namedarg (name args)
  (declare (xargs :guard (and (stringp name)
                              (vl-namedarglist-p args))))
  (let ((__function__ 'vl-find-namedarg))
    (declare (ignorable __function__))
    (cond ((atom args) nil)
          ((equal (vl-namedarg->name (car args))
                  name)
           (vl-namedarg-fix (car args)))
          (t (vl-find-namedarg name (cdr args))))))

Theorem: vl-find-namedarg-under-iff

(defthm vl-find-namedarg-under-iff
  (iff (vl-find-namedarg name args)
       (member-equal name (vl-namedarglist->names args))))

Theorem: vl-namedarg-p-of-vl-find-namedarg

(defthm vl-namedarg-p-of-vl-find-namedarg
  (equal (vl-namedarg-p (vl-find-namedarg name args))
         (if (member-equal name (vl-namedarglist->names args))
             t
           nil)))

Theorem: vl-find-namedarg-of-vl-namedarglist-fix-args

(defthm vl-find-namedarg-of-vl-namedarglist-fix-args
  (equal (vl-find-namedarg name (vl-namedarglist-fix args))
         (vl-find-namedarg name args)))

Theorem: vl-find-namedarg-vl-namedarglist-equiv-congruence-on-args

(defthm vl-find-namedarg-vl-namedarglist-equiv-congruence-on-args
  (implies (vl-namedarglist-equiv args args-equiv)
           (equal (vl-find-namedarg name args)
                  (vl-find-namedarg name args-equiv)))
  :rule-classes :congruence)