• 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-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

• 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, 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)