		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 ss) → new-x
Arguments: x — Guard (vl-module-p x).; ss — Guard (vl-scopestack-p ss).
Returns: new-x — Same as x, but perhaps with more warnings.
Type (vl-module-p new-x).

Definitions and Theorems

Function: vl-module-duplicate-detect

(defun vl-module-duplicate-detect (x ss)
 (declare (xargs :guard (and (vl-module-p x)
                             (vl-scopestack-p ss))))
 (let ((__function__ 'vl-module-duplicate-detect))
  (declare (ignorable __function__))
  (b*
   (((vl-module x) (vl-module-fix x))
    (ss (vl-scopestack-push x ss))
    (modinsts (vl-modinstlist-remove-interfaces x.modinsts ss))
    (gateinsts-fix
         (vl-duplicate-detect-strip-gateinsts x.gateinsts))
    (modinsts-fix (vl-duplicate-detect-strip-modinsts modinsts))
    (assigns-fix (vl-duplicate-detect-strip-assigns x.assigns))
    (always-fix (vl-duplicate-detect-strip-alwayses x.alwayses))
    (initial-fix (vl-duplicate-detect-strip-initials x.initials))
    (final-fix (vl-duplicate-detect-strip-finals x.finals))
    (alias-fix (vl-duplicate-detect-strip-aliases x.aliases))
    (assert-fix (vl-duplicate-detect-strip-assertions x.assertions))
    (cassert-fix
         (vl-duplicate-detect-strip-cassertions x.cassertions))
    (property-fix
         (vl-duplicate-detect-strip-properties x.properties))
    (sequence-fix (vl-duplicate-detect-strip-sequences x.sequences))
    (gateinst-dupes (duplicated-members gateinsts-fix))
    (modinst-dupes (duplicated-members modinsts-fix))
    (assign-dupes (duplicated-members assigns-fix))
    (always-dupes (duplicated-members always-fix))
    (initial-dupes (duplicated-members initial-fix))
    (final-dupes (duplicated-members final-fix))
    (alias-dupes (duplicated-members alias-fix))
    (assert-dupes (duplicated-members assert-fix))
    (cassert-dupes (duplicated-members cassert-fix))
    (property-dupes (duplicated-members property-fix))
    (sequence-dupes (duplicated-members sequence-fix))
    (gateinst-warnings
         (vl-duplicate-warnings gateinst-dupes
                                gateinsts-fix x.gateinsts))
    (modinst-warnings
        (vl-duplicate-warnings modinst-dupes modinsts-fix modinsts))
    (assign-warnings
         (vl-duplicate-warnings assign-dupes assigns-fix x.assigns))
    (always-warnings
         (vl-duplicate-warnings always-dupes always-fix x.alwayses))
    (initial-warnings
       (vl-duplicate-warnings initial-dupes initial-fix x.initials))
    (final-warnings
         (vl-duplicate-warnings final-dupes final-fix x.finals))
    (alias-warnings
         (vl-duplicate-warnings alias-dupes alias-fix x.aliases))
    (assert-warnings
       (vl-duplicate-warnings assert-dupes assert-fix x.assertions))
    (cassert-warnings
         (vl-duplicate-warnings cassert-dupes
                                cassert-fix x.cassertions))
    (property-warnings
         (vl-duplicate-warnings property-dupes
                                property-fix x.properties))
    (sequence-warnings
         (vl-duplicate-warnings sequence-dupes
                                sequence-fix x.sequences))
    (warnings (append gateinst-warnings modinst-warnings
                      assign-warnings always-warnings
                      initial-warnings final-warnings
                      alias-warnings assert-warnings
                      cassert-warnings property-warnings
                      sequence-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
  (b* ((new-x (vl-module-duplicate-detect x ss)))
    (vl-module-p new-x))
  :rule-classes :rewrite)