		Search-engine friendly clone of the ACL2 documentation.

Argresolve

Vl-check-blankargs

Warn about expressions connected to blank ports and for blanks connected to non-blank, non-output ports.

Signature
(vl-check-blankargs args ports inst warnings) → warnings
Arguments: args — plainargs for a module instance, which should already be annotated with their directions.
Guard (vl-plainarglist-p args).; ports — corresponding ports for the submodule.
Guard (vl-portlist-p ports).; inst — just a context for warnings.
Guard (vl-modinst-p inst).; warnings — warnings accumulator.
Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).

We historically warned about blank arguments connected to any port. However, it seems reasonably common that a module will produce outputs you don't care about, and connecting a blank to such an output seems like a very reasonable thing to do. So, we no longer warn about blanks that are connected to output ports.

Either of these situations is semantically well-formed and relatively easy to handle; see blankargs. But they are also bizarre, and at least would seem to indicate a situation that could be optimized. So, if we see either of these cases, we add a non-fatal warning explaining the problem.

Definitions and Theorems

Function: vl-check-blankargs

(defun vl-check-blankargs (args ports inst warnings)
 (declare (xargs :guard (and (vl-plainarglist-p args)
                             (vl-portlist-p ports)
                             (vl-modinst-p inst)
                             (vl-warninglist-p warnings))))
 (declare (xargs :guard (same-lengthp args ports)))
 (let ((__function__ 'vl-check-blankargs))
  (declare (ignorable __function__))
  (b*
   (((when (atom args)) (ok))
    (inst (vl-modinst-fix inst))
    (port1 (vl-port-fix (car ports)))
    ((when (eq (tag port1) :vl-interfaceport))
     (vl-check-blankargs (cdr args)
                         (cdr ports)
                         inst warnings))
    ((vl-regularport port1) port1)
    ((vl-plainarg arg1) (car args))
    (warnings
     (if
      (and arg1.expr (not port1.expr))
      (warn
       :type :vl-warn-blank
       :msg
       "~a0 connects the expression ~a1 to the blank port at ~
                        ~l2."
       :args (list inst arg1.expr port1.loc))
      (ok)))
    (warnings
     (if
      (and port1.expr (not arg1.expr)
           (not (eq arg1.dir :vl-output)))
      (warn
       :type :vl-warn-blank
       :msg
       "~a0 gives a blank expression for non-blank port ~a1 (port direction: ~s2)."
       :args (list inst port1 arg1.dir))
      (ok))))
   (vl-check-blankargs (cdr args)
                       (cdr ports)
                       inst warnings))))

Theorem: vl-warninglist-p-of-vl-check-blankargs

(defthm vl-warninglist-p-of-vl-check-blankargs
  (b* ((warnings (vl-check-blankargs args ports inst warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-check-blankargs-of-vl-plainarglist-fix-args

(defthm vl-check-blankargs-of-vl-plainarglist-fix-args
  (equal (vl-check-blankargs (vl-plainarglist-fix args)
                             ports inst warnings)
         (vl-check-blankargs args ports inst warnings)))

Theorem: vl-check-blankargs-vl-plainarglist-equiv-congruence-on-args

(defthm vl-check-blankargs-vl-plainarglist-equiv-congruence-on-args
  (implies
       (vl-plainarglist-equiv args args-equiv)
       (equal (vl-check-blankargs args ports inst warnings)
              (vl-check-blankargs args-equiv ports inst warnings)))
  :rule-classes :congruence)

Theorem: vl-check-blankargs-of-vl-portlist-fix-ports

(defthm vl-check-blankargs-of-vl-portlist-fix-ports
  (equal (vl-check-blankargs args (vl-portlist-fix ports)
                             inst warnings)
         (vl-check-blankargs args ports inst warnings)))

Theorem: vl-check-blankargs-vl-portlist-equiv-congruence-on-ports

(defthm vl-check-blankargs-vl-portlist-equiv-congruence-on-ports
  (implies
       (vl-portlist-equiv ports ports-equiv)
       (equal (vl-check-blankargs args ports inst warnings)
              (vl-check-blankargs args ports-equiv inst warnings)))
  :rule-classes :congruence)

Theorem: vl-check-blankargs-of-vl-modinst-fix-inst

(defthm vl-check-blankargs-of-vl-modinst-fix-inst
  (equal (vl-check-blankargs args ports (vl-modinst-fix inst)
                             warnings)
         (vl-check-blankargs args ports inst warnings)))

Theorem: vl-check-blankargs-vl-modinst-equiv-congruence-on-inst

(defthm vl-check-blankargs-vl-modinst-equiv-congruence-on-inst
  (implies
       (vl-modinst-equiv inst inst-equiv)
       (equal (vl-check-blankargs args ports inst warnings)
              (vl-check-blankargs args ports inst-equiv warnings)))
  :rule-classes :congruence)

Theorem: vl-check-blankargs-of-vl-warninglist-fix-warnings

(defthm vl-check-blankargs-of-vl-warninglist-fix-warnings
  (equal (vl-check-blankargs args ports
                             inst (vl-warninglist-fix warnings))
         (vl-check-blankargs args ports inst warnings)))

Theorem: vl-check-blankargs-vl-warninglist-equiv-congruence-on-warnings

(defthm
     vl-check-blankargs-vl-warninglist-equiv-congruence-on-warnings
  (implies
       (vl-warninglist-equiv warnings warnings-equiv)
       (equal (vl-check-blankargs args ports inst warnings)
              (vl-check-blankargs args ports inst warnings-equiv)))
  :rule-classes :congruence)