• 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-create-namedarg-for-dotstar
                • Vl-create-namedargs-for-dotstar
              • 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-expand-dotstar-arguments

Expand .* style arguments into explicit .foo(foo) format.

Signature

(vl-expand-dotstar-arguments args ss ports warnings inst) 
  → 
(mv successp warnings new-args)

Arguments

args — The explicit arguments besides the .*, i.e., .foo(1), .bar(2), ....
    Guard (vl-namedarglist-p args).

ss — Scopestack for the superior module.
    Guard (vl-scopestack-p ss).

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

warnings — Warnings accumulator.
    Guard (vl-warninglist-p warnings).

inst — Just a context for warnings.
    Guard (vl-modinst-p inst).

Returns

successp — Type (booleanp successp).

warnings — Type (vl-warninglist-p warnings).

new-args — Type (vl-namedarglist-p new-args).

Definitions and Theorems

Function: vl-expand-dotstar-arguments

(defun vl-expand-dotstar-arguments (args ss ports warnings inst)
 (declare (xargs :guard (and (vl-namedarglist-p args)
                             (vl-scopestack-p ss)
                             (vl-portlist-p ports)
                             (vl-warninglist-p warnings)
                             (vl-modinst-p inst))))
 (let ((__function__ 'vl-expand-dotstar-arguments))
  (declare (ignorable __function__))
  (b*
   ((args (vl-namedarglist-fix args))
    ((vl-modinst inst)
     (vl-modinst-fix inst))
    (portnames (vl-portlist->names ports))
    ((when (member nil portnames))
     (mv
      nil
      (fatal
       :type :vl-named-args-for-unnamed-ports
       :msg
       "~a0 has named arguments, which is illegal since ~m1 ~
                         has unnamed ports."
       :args (list inst inst.modname))
      args))
    (argnames (vl-namedarglist->names args))
    (missing (difference (mergesort portnames)
                         (mergesort argnames)))
    (warnings
     (if missing warnings
      (warn
       :type :vl-warn-empty-dotstar
       :msg
       "~a0 mentions .*, but explicitly connects all of ~
                               the ports of ~m1, so the .* isn't doing anything."
       :args (list inst inst.modname))))
    ((mv okp warnings inferred-args)
     (vl-create-namedargs-for-dotstar missing ss warnings inst))
    ((unless okp) (mv nil warnings args))
    (new-args (append inferred-args args)))
   (mv t warnings new-args))))

Theorem: booleanp-of-vl-expand-dotstar-arguments.successp

(defthm booleanp-of-vl-expand-dotstar-arguments.successp
  (b* (((mv ?successp ?warnings ?new-args)
        (vl-expand-dotstar-arguments args ss ports warnings inst)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-expand-dotstar-arguments.warnings

(defthm vl-warninglist-p-of-vl-expand-dotstar-arguments.warnings
  (b* (((mv ?successp ?warnings ?new-args)
        (vl-expand-dotstar-arguments args ss ports warnings inst)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-namedarglist-p-of-vl-expand-dotstar-arguments.new-args

(defthm vl-namedarglist-p-of-vl-expand-dotstar-arguments.new-args
  (b* (((mv ?successp ?warnings ?new-args)
        (vl-expand-dotstar-arguments args ss ports warnings inst)))
    (vl-namedarglist-p new-args))
  :rule-classes :rewrite)

Theorem: vl-expand-dotstar-arguments-of-vl-namedarglist-fix-args

(defthm vl-expand-dotstar-arguments-of-vl-namedarglist-fix-args
  (equal (vl-expand-dotstar-arguments (vl-namedarglist-fix args)
                                      ss ports warnings inst)
         (vl-expand-dotstar-arguments args ss ports warnings inst)))

Theorem: vl-expand-dotstar-arguments-vl-namedarglist-equiv-congruence-on-args

(defthm
 vl-expand-dotstar-arguments-vl-namedarglist-equiv-congruence-on-args
 (implies
  (vl-namedarglist-equiv args args-equiv)
  (equal
   (vl-expand-dotstar-arguments args ss ports warnings inst)
   (vl-expand-dotstar-arguments args-equiv ss ports warnings inst)))
 :rule-classes :congruence)

Theorem: vl-expand-dotstar-arguments-of-vl-scopestack-fix-ss

(defthm vl-expand-dotstar-arguments-of-vl-scopestack-fix-ss
  (equal (vl-expand-dotstar-arguments args (vl-scopestack-fix ss)
                                      ports warnings inst)
         (vl-expand-dotstar-arguments args ss ports warnings inst)))

Theorem: vl-expand-dotstar-arguments-vl-scopestack-equiv-congruence-on-ss

(defthm
   vl-expand-dotstar-arguments-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal
   (vl-expand-dotstar-arguments args ss ports warnings inst)
   (vl-expand-dotstar-arguments args ss-equiv ports warnings inst)))
 :rule-classes :congruence)

Theorem: vl-expand-dotstar-arguments-of-vl-portlist-fix-ports

(defthm vl-expand-dotstar-arguments-of-vl-portlist-fix-ports
 (equal (vl-expand-dotstar-arguments args ss (vl-portlist-fix ports)
                                     warnings inst)
        (vl-expand-dotstar-arguments args ss ports warnings inst)))

Theorem: vl-expand-dotstar-arguments-vl-portlist-equiv-congruence-on-ports

(defthm
  vl-expand-dotstar-arguments-vl-portlist-equiv-congruence-on-ports
 (implies
  (vl-portlist-equiv ports ports-equiv)
  (equal
   (vl-expand-dotstar-arguments args ss ports warnings inst)
   (vl-expand-dotstar-arguments args ss ports-equiv warnings inst)))
 :rule-classes :congruence)

Theorem: vl-expand-dotstar-arguments-of-vl-warninglist-fix-warnings

(defthm vl-expand-dotstar-arguments-of-vl-warninglist-fix-warnings
  (equal (vl-expand-dotstar-arguments
              args
              ss ports (vl-warninglist-fix warnings)
              inst)
         (vl-expand-dotstar-arguments args ss ports warnings inst)))

Theorem: vl-expand-dotstar-arguments-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-expand-dotstar-arguments-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal
   (vl-expand-dotstar-arguments args ss ports warnings inst)
   (vl-expand-dotstar-arguments args ss ports warnings-equiv inst)))
 :rule-classes :congruence)

Theorem: vl-expand-dotstar-arguments-of-vl-modinst-fix-inst

(defthm vl-expand-dotstar-arguments-of-vl-modinst-fix-inst
  (equal (vl-expand-dotstar-arguments
              args
              ss ports warnings (vl-modinst-fix inst))
         (vl-expand-dotstar-arguments args ss ports warnings inst)))

Theorem: vl-expand-dotstar-arguments-vl-modinst-equiv-congruence-on-inst

(defthm
    vl-expand-dotstar-arguments-vl-modinst-equiv-congruence-on-inst
 (implies
  (vl-modinst-equiv inst inst-equiv)
  (equal
   (vl-expand-dotstar-arguments args ss ports warnings inst)
   (vl-expand-dotstar-arguments args ss ports warnings inst-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-create-namedarg-for-dotstar

Create a single missing argument for a .* connection.

Vl-create-namedargs-for-dotstar

Create the arguments that .* expands to.