		Search-engine friendly clone of the ACL2 documentation.

Argresolve

Vl-convert-namedargs

Coerce arguments into plain (positional) style.

Signature
(vl-convert-namedargs x ss ports warnings inst) → (mv successp warnings new-x)
Arguments: x — arguments of a module instance, named or plain.
Guard (vl-arguments-p x).; ss — scope stack 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-x — Type (vl-arguments-p new-x).

We used to require that every port had a connection, and otherwise caused a fatal warning. This is no longer the case.

A missing port is obviously a concern and we should at least cause a warning. But the Verilog-2005 standard does not seem to say that it is an error, and at least some other Verilog tools, like Verilog-XL and NCVerilog, merely warn about the situation and then simply treat the port as unconnected.

To be able to handle designs that do this bad thing, we now also tolerate named arguments with missing ports, and only issue non-fatal warnings.

Definitions and Theorems

Function: vl-convert-namedargs

(defun vl-convert-namedargs (x ss ports warnings inst)
 (declare (xargs :guard (and (vl-arguments-p x)
                             (vl-scopestack-p ss)
                             (vl-portlist-p ports)
                             (vl-warninglist-p warnings)
                             (vl-modinst-p inst))))
 (declare (ignorable ss))
 (let ((__function__ 'vl-convert-namedargs))
  (declare (ignorable __function__))
  (b*
   ((x (vl-arguments-fix x))
    (inst (vl-modinst-fix inst))
    ((vl-modinst inst) inst)
    (x (vl-arguments-case x :vl-arguments-plain
                          (if (atom x.args)
                              (make-vl-arguments-named :args nil
                                                       :starp nil)
                            x)
                          :otherwise x))
    ((when (eq (vl-arguments-kind x)
               :vl-arguments-plain))
     (mv t (ok) x))
    ((mv okp warnings args)
     (if (vl-arguments-named->starp x)
         (vl-expand-dotstar-arguments (vl-arguments-named->args x)
                                      ss ports warnings inst)
       (mv t (ok)
           (vl-arguments-named->args x))))
    ((unless okp) (mv nil warnings x))
    (formal-names (vl-portlist->names ports))
    (actual-names (vl-namedarglist->names args))
    (sorted-formals (mergesort formal-names))
    (sorted-actuals (mergesort actual-names))
    ((when (member nil (vl-portlist->names ports)))
     (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))
      x))
    ((unless (mbe :logic (uniquep actual-names)
                  :exec (same-lengthp actual-names sorted-actuals)))
     (mv
      nil
      (fatal
       :type
       :vl-instance-multiple-connections :msg
       "~a0 illegally has multiple connections for port~s1 ~
                         ~&2."
       :args
       (let ((dupes (duplicated-members actual-names)))
         (list inst (if (vl-plural-p dupes) "s" "")
               dupes)))
      x))
    ((unless (subset sorted-actuals sorted-formals))
     (b* ((extra (difference sorted-actuals sorted-formals)))
      (mv
       nil
       (fatal
        :type :vl-instance-nonexistent-port
        :msg
        "~a0 illegally connects to the following ~s1 in ~
                           ~m2: ~&3"
        :args (list inst
                    (if (vl-plural-p extra)
                        "ports, which do not exist"
                      "port, which does not exist")
                    inst.modname extra))
       x)))
    (warnings
        (if (subset sorted-formals sorted-actuals)
            (ok)
          (b* ((missing (difference sorted-formals sorted-actuals)))
            (warn :type :vl-instance-missing-ports
                  :msg "~a0 omits the following ~s1 from ~m2: ~&3"
                  :args (list inst
                              (if (vl-plural-p missing)
                                  "ports"
                                "port")
                              inst.modname missing)))))
    (plainargs
     (mbe
       :logic
       (vl-convert-namedargs-aux args ports)
       :exec
       (if (< (len args) 20)
           (vl-convert-namedargs-aux args ports)
         (b* ((alist (vl-make-namedarg-alist args))
              (ans (vl-convert-namedargs-aux-fal args alist ports)))
           (fast-alist-free alist)
           ans))))
    (new-x (make-vl-arguments-plain :args plainargs)))
   (mv t (ok) new-x))))

Theorem: booleanp-of-vl-convert-namedargs.successp

(defthm booleanp-of-vl-convert-namedargs.successp
  (b* (((mv ?successp ?warnings ?new-x)
        (vl-convert-namedargs x ss ports warnings inst)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-convert-namedargs.warnings

(defthm vl-warninglist-p-of-vl-convert-namedargs.warnings
  (b* (((mv ?successp ?warnings ?new-x)
        (vl-convert-namedargs x ss ports warnings inst)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-arguments-p-of-vl-convert-namedargs.new-x

(defthm vl-arguments-p-of-vl-convert-namedargs.new-x
  (b* (((mv ?successp ?warnings ?new-x)
        (vl-convert-namedargs x ss ports warnings inst)))
    (vl-arguments-p new-x))
  :rule-classes :rewrite)

Theorem: vl-arguments-kind-of-vl-convert-namedargs

(defthm vl-arguments-kind-of-vl-convert-namedargs
  (b* (((mv ?successp ?warnings ?new-x)
        (vl-convert-namedargs x ss ports warnings inst)))
    (implies successp
             (equal (vl-arguments-kind new-x)
                    :vl-arguments-plain)))
  :rule-classes :rewrite)

Theorem: vl-convert-namedargs-of-vl-arguments-fix-x

(defthm vl-convert-namedargs-of-vl-arguments-fix-x
  (equal (vl-convert-namedargs (vl-arguments-fix x)
                               ss ports warnings inst)
         (vl-convert-namedargs x ss ports warnings inst)))

Theorem: vl-convert-namedargs-vl-arguments-equiv-congruence-on-x

(defthm vl-convert-namedargs-vl-arguments-equiv-congruence-on-x
 (implies
      (vl-arguments-equiv x x-equiv)
      (equal (vl-convert-namedargs x ss ports warnings inst)
             (vl-convert-namedargs x-equiv ss ports warnings inst)))
 :rule-classes :congruence)

Theorem: vl-convert-namedargs-of-vl-scopestack-fix-ss

(defthm vl-convert-namedargs-of-vl-scopestack-fix-ss
  (equal (vl-convert-namedargs x (vl-scopestack-fix ss)
                               ports warnings inst)
         (vl-convert-namedargs x ss ports warnings inst)))

Theorem: vl-convert-namedargs-vl-scopestack-equiv-congruence-on-ss

(defthm vl-convert-namedargs-vl-scopestack-equiv-congruence-on-ss
 (implies
      (vl-scopestack-equiv ss ss-equiv)
      (equal (vl-convert-namedargs x ss ports warnings inst)
             (vl-convert-namedargs x ss-equiv ports warnings inst)))
 :rule-classes :congruence)

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

(defthm vl-convert-namedargs-of-vl-portlist-fix-ports
  (equal (vl-convert-namedargs x ss (vl-portlist-fix ports)
                               warnings inst)
         (vl-convert-namedargs x ss ports warnings inst)))

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

(defthm vl-convert-namedargs-vl-portlist-equiv-congruence-on-ports
 (implies
      (vl-portlist-equiv ports ports-equiv)
      (equal (vl-convert-namedargs x ss ports warnings inst)
             (vl-convert-namedargs x ss ports-equiv warnings inst)))
 :rule-classes :congruence)

Theorem: vl-convert-namedargs-of-vl-warninglist-fix-warnings

(defthm vl-convert-namedargs-of-vl-warninglist-fix-warnings
 (equal
      (vl-convert-namedargs x ss ports (vl-warninglist-fix warnings)
                            inst)
      (vl-convert-namedargs x ss ports warnings inst)))

Theorem: vl-convert-namedargs-vl-warninglist-equiv-congruence-on-warnings

(defthm
   vl-convert-namedargs-vl-warninglist-equiv-congruence-on-warnings
 (implies
      (vl-warninglist-equiv warnings warnings-equiv)
      (equal (vl-convert-namedargs x ss ports warnings inst)
             (vl-convert-namedargs x ss ports warnings-equiv inst)))
 :rule-classes :congruence)

Theorem: vl-convert-namedargs-of-vl-modinst-fix-inst

(defthm vl-convert-namedargs-of-vl-modinst-fix-inst
 (equal
      (vl-convert-namedargs x
                            ss ports warnings (vl-modinst-fix inst))
      (vl-convert-namedargs x ss ports warnings inst)))

Theorem: vl-convert-namedargs-vl-modinst-equiv-congruence-on-inst

(defthm vl-convert-namedargs-vl-modinst-equiv-congruence-on-inst
 (implies
      (vl-modinst-equiv inst inst-equiv)
      (equal (vl-convert-namedargs x ss ports warnings inst)
             (vl-convert-namedargs x ss ports warnings inst-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-expand-dotstar-arguments: Expand .* style arguments into explicit .foo(foo) format.
Vl-convert-namedargs-aux: Change a named argument list into an equivalent plain (positional) argument list.
Vl-find-namedarg: Look up an argument by name in a named argument list.
Vl-convert-namedargs-aux-fal