• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
        • Vl-lintconfig-p
        • Lucid
        • Skip-detection
        • Vl-lintresult-p
        • Lint-warning-suppression
        • Condcheck
        • Selfassigns
        • Leftright-check
        • Dupeinst-check
          • Vl-dupeinst-alistp
          • Vl-modulelist-dupeinst-check
          • Vl-dupeinst-key-p
          • Vl-maybe-warn-dupeinst
            • Vl-modinstlist-fixed-up-outs
          • Vl-warnings-for-dupeinst-alist
          • Vl-make-dupeinst-alist
          • Vl-module-dupeinst-check
          • Vl-dupeinst-trivial-p
          • Vl-design-dupeinst-check
          • Vl-pp-dupeinst-key
          • Vl-pp-dupeinst-alist
        • Oddexpr-check
        • Remove-toohard
        • Qmarksize-check
        • Portcheck
        • Duplicate-detect
        • Vl-print-certain-warnings
        • Duperhs-check
        • *vl-lint-help*
        • Lint-stmt-rewrite
        • Drop-missing-submodules
        • Check-case
        • Drop-user-submodules
        • Check-namespace
        • Vl-lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

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