		Search-engine friendly clone of the ACL2 documentation.

Dupeinst-check

Vl-maybe-warn-dupeinst

Possibly add warnings about a group of module instances.

Signature
(vl-maybe-warn-dupeinst key modinsts ss warnings) → new-warnings
Arguments: key — The shared key for a group of modinsts.
Guard (vl-dupeinst-key-p key).; modinsts — The modinsts that share this key.
Guard (vl-modinstlist-p modinsts).; ss — Scopestack for doing module lookups.
Guard (vl-scopestack-p ss).; warnings — The warnings accumulator to extend.
Guard (vl-warninglist-p warnings).
Returns: new-warnings — Type (vl-warninglist-p new-warnings).

Modinsts might not have multiple entries, in which case there is nothing to do and we just return warnings unchanged. Otherwise, we issue a warning about the modules.

Definitions and Theorems

Function: vl-maybe-warn-dupeinst

(defun vl-maybe-warn-dupeinst (key modinsts ss warnings)
 (declare (xargs :guard (and (vl-dupeinst-key-p key)
                             (vl-modinstlist-p modinsts)
                             (vl-scopestack-p ss)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-maybe-warn-dupeinst))
  (declare (ignorable __function__))
  (b*
   (((when (or (atom modinsts)
               (atom (cdr modinsts))))
     (ok))
    (mod
       (vl-scopestack-find-definition (vl-dupeinst-key->modname key)
                                      ss))
    ((when (eq (tag mod) :vl-interface))
     (and *dupeinst-check-debug*
          (vl-cw-ps-seq
               (vl-cw "Skipping ~s0 because it's an interface:~%")
               (vl-pp-dupeinst-key key)
               (vl-cw "~%")))
     (ok))
    ((when (and (eq (tag mod) :vl-module)
                (atom (vl-module->ports mod))))
     (and *dupeinst-check-debug*
          (vl-cw-ps-seq
               (vl-cw "Skipping ~s0 because it has no ports.~%")
               (vl-pp-dupeinst-key key)
               (vl-cw "~%")))
     (ok))
    (fixed-up-outs (vl-modinstlist-fixed-up-outs modinsts))
    (dupes (duplicated-members fixed-up-outs))
    (modname (vl-dupeinst-key->modname key))
    (minor-p (vl-dupeinst-trivial-p modname)))
   (warn :type
         (if (consp dupes)
             (if minor-p :vl-warn-same-ports-minor
               :vl-warn-same-ports)
           (if minor-p :vl-warn-same-inputs-minor
             :vl-warn-same-inputs))
         :msg "Found instances of the same module with ~s0:~%~%~s1"
         :args
         (list (if (consp dupes)
                   "the same arguments"
                 "the same inputs (but different outputs)")
               (str::prefix-lines
                    (with-local-ps (vl-ps-update-autowrap-col 200)
                                   (vl-pp-modinstlist modinsts nil))
                    "     ")
               modinsts)))))

Theorem: vl-warninglist-p-of-vl-maybe-warn-dupeinst

(defthm vl-warninglist-p-of-vl-maybe-warn-dupeinst
 (b*
  ((new-warnings (vl-maybe-warn-dupeinst key modinsts ss warnings)))
  (vl-warninglist-p new-warnings))
 :rule-classes :rewrite)

Subtopics

Vl-modinstlist-fixed-up-outs: Extract the vl-expr-striped outputs from each module instance.