		Search-engine friendly clone of the ACL2 documentation.

Shadowcheck

Vl-shadowcheck-design

Signature
(vl-shadowcheck-design x) → new-x
Arguments: x — Guard (vl-design-p x).
Returns: new-x — Type (vl-design-p new-x).

Definitions and Theorems

Function: vl-shadowcheck-design

(defun vl-shadowcheck-design (x)
  (declare (xargs :guard (vl-design-p x)))
  (let ((__function__ 'vl-shadowcheck-design))
    (declare (ignorable __function__))
    (b* (((vl-design x) (vl-design-fix x))
         (warnings x.warnings)
         (st (make-vl-shadowcheck-state
                  :lexscopes (list (vl-empty-lexscope))
                  :ss (vl-scopestack-init x)
                  :design x))
         (warnings (vl-scope-nameclash-warnings x x warnings))
         ((mv st warnings)
          (vl-shadowcheck-imports x.imports st warnings))
         ((mv st warnings)
          (vl-shadowcheck-declare-typedefs x.typedefs st warnings))
         ((mv st warnings)
          (vl-shadowcheck-vardecls x.vardecls st warnings))
         ((mv st warnings)
          (vl-shadowcheck-paramdecls x.paramdecls st warnings))
         ((mv st warnings)
          (vl-shadowcheck-fundecls x.fundecls st warnings))
         ((mv st warnings)
          (vl-shadowcheck-taskdecls x.taskdecls st warnings))
         ((mv st warnings)
          (vl-shadowcheck-dpiimports x.dpiimports st warnings))
         ((mv st mods)
          (vl-shadowcheck-modules x.mods st))
         ((mv st interfaces)
          (vl-shadowcheck-interfaces x.interfaces st))
         (?st (vl-shadowcheck-pop-scope st))
         (- (vl-scopestacks-free))
         (new-x (change-vl-design x
                                  :mods mods
                                  :interfaces interfaces
                                  :warnings warnings)))
      (vl-design-deltemps new-x))))

Theorem: vl-design-p-of-vl-shadowcheck-design

(defthm vl-design-p-of-vl-shadowcheck-design
  (b* ((new-x (vl-shadowcheck-design x)))
    (vl-design-p new-x))
  :rule-classes :rewrite)

Theorem: vl-shadowcheck-design-of-vl-design-fix-x

(defthm vl-shadowcheck-design-of-vl-design-fix-x
  (equal (vl-shadowcheck-design (vl-design-fix x))
         (vl-shadowcheck-design x)))

Theorem: vl-shadowcheck-design-vl-design-equiv-congruence-on-x

(defthm vl-shadowcheck-design-vl-design-equiv-congruence-on-x
  (implies (vl-design-equiv x x-equiv)
           (equal (vl-shadowcheck-design x)
                  (vl-shadowcheck-design x-equiv)))
  :rule-classes :congruence)