• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • 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-convert-namedargs-aux-fal

Signature

(vl-convert-namedargs-aux-fal args alist ports) → *

Arguments

args — Named arguments for some module instance.
    Guard (vl-namedarglist-p args).

alist — Guard (equal alist (vl-make-namedarg-alist args)).

ports — Ports of the submodule.
    Guard (vl-portlist-p ports).

Definitions and Theorems

Function: vl-convert-namedargs-aux-fal

(defun vl-convert-namedargs-aux-fal (args alist ports)
 (declare
   (xargs :guard (and (vl-namedarglist-p args)
                      (vl-portlist-p ports)
                      (equal alist (vl-make-namedarg-alist args)))))
 (declare
      (xargs :guard (not (member nil (vl-portlist->names ports)))))
 (let ((__function__ 'vl-convert-namedargs-aux-fal))
  (declare (ignorable __function__))
  (mbe
   :logic
   (vl-convert-namedargs-aux args ports)
   :exec
   (b*
    (((when (atom ports)) nil)
     (namedarg (vl-fast-find-namedarg (vl-port->name (car ports))
                                      args alist))
     (plainarg
          (if namedarg
              (make-vl-plainarg :expr (vl-namedarg->expr namedarg)
                                :atts (vl-namedarg->atts namedarg))
            (make-vl-plainarg :expr nil
                              :atts '(("VL_MISSING_CONNECTION"))))))
    (cons plainarg
          (vl-convert-namedargs-aux-fal args alist (cdr ports)))))))

Theorem: vl-convert-namedargs-aux-fal-of-vl-namedarglist-fix-args

(defthm vl-convert-namedargs-aux-fal-of-vl-namedarglist-fix-args
  (equal (vl-convert-namedargs-aux-fal (vl-namedarglist-fix args)
                                       alist ports)
         (vl-convert-namedargs-aux-fal args alist ports)))

Theorem: vl-convert-namedargs-aux-fal-vl-namedarglist-equiv-congruence-on-args

(defthm
 vl-convert-namedargs-aux-fal-vl-namedarglist-equiv-congruence-on-args
 (implies
      (vl-namedarglist-equiv args args-equiv)
      (equal (vl-convert-namedargs-aux-fal args alist ports)
             (vl-convert-namedargs-aux-fal args-equiv alist ports)))
 :rule-classes :congruence)

Theorem: vl-convert-namedargs-aux-fal-of-vl-portlist-fix-ports

(defthm vl-convert-namedargs-aux-fal-of-vl-portlist-fix-ports
 (equal
   (vl-convert-namedargs-aux-fal args alist (vl-portlist-fix ports))
   (vl-convert-namedargs-aux-fal args alist ports)))

Theorem: vl-convert-namedargs-aux-fal-vl-portlist-equiv-congruence-on-ports

(defthm
 vl-convert-namedargs-aux-fal-vl-portlist-equiv-congruence-on-ports
 (implies
      (vl-portlist-equiv ports ports-equiv)
      (equal (vl-convert-namedargs-aux-fal args alist ports)
             (vl-convert-namedargs-aux-fal args alist ports-equiv)))
 :rule-classes :congruence)