		Search-engine friendly clone of the ACL2 documentation.

Duplicate-detect

Vl-module-duplicate-detect

Detect duplicate assignments and instances throughout a module.

Signature
(vl-module-duplicate-detect x) → new-x
Arguments: x — Guard (vl-module-p x).
Returns: new-x — Same as x, but perhaps with more warnings.
Type (vl-module-p new-x), given the guard.

Definitions and Theorems

Function: vl-module-duplicate-detect

(defun vl-module-duplicate-detect (x)
 (declare (xargs :guard (vl-module-p x)))
 (let ((__function__ 'vl-module-duplicate-detect))
  (declare (ignorable __function__))
  (b*
   (((vl-module x) x)
    (gateinsts-fix (vl-gateinstlist-strip x.gateinsts))
    (modinsts-fix (vl-modinstlist-strip x.modinsts))
    (assigns-fix (vl-assignlist-strip x.assigns))
    (gateinst-dupes (duplicated-members gateinsts-fix))
    (modinst-dupes (duplicated-members modinsts-fix))
    (assign-dupes (duplicated-members assigns-fix))
    ((unless (or gateinst-dupes
                 modinst-dupes assign-dupes))
     x)
    (gate-warnings (and gateinst-dupes
                        (vl-duplicate-gateinst-warnings
                             gateinst-dupes
                             gateinsts-fix x.gateinsts x.name)))
    (mod-warnings (and modinst-dupes
                       (vl-duplicate-modinst-warnings
                            modinst-dupes
                            modinsts-fix x.modinsts x.name)))
    (ass-warnings
     (and
       assign-dupes
       (vl-duplicate-assign-warnings assign-dupes
                                     assigns-fix x.assigns x.name)))
    (warnings (append gate-warnings
                      mod-warnings ass-warnings x.warnings)))
   (change-vl-module x
                     :warnings warnings))))

Theorem: vl-module-p-of-vl-module-duplicate-detect

(defthm vl-module-p-of-vl-module-duplicate-detect
  (implies (and (force (vl-module-p x)))
           (b* ((new-x (vl-module-duplicate-detect x)))
             (vl-module-p new-x)))
  :rule-classes :rewrite)