		Search-engine friendly clone of the ACL2 documentation.

Weirdint-elim

Vl-module-weirdint-elim

Signature
(vl-module-weirdint-elim x) → (mv new-x addmods)
Arguments: x — Guard (vl-module-p x).
Returns: new-x — Type (vl-module-p new-x).; addmods — Type (vl-modulelist-p addmods).

Definitions and Theorems

Function: vl-module-weirdint-elim

(defun vl-module-weirdint-elim (x)
 (declare (xargs :guard (vl-module-p x)))
 (let ((__function__ 'vl-module-weirdint-elim))
  (declare (ignorable __function__))
  (b*
   ((x (vl-module-fix x))
    ((when (vl-module->hands-offp x))
     (mv x nil))
    ((vl-module x) x)
    (warnings x.warnings)
    ((mv warnings assigns-changedp assigns)
     (vl-assignlist-weirdint-elim x.assigns warnings))
    ((mv warnings modinsts-changedp modinsts)
     (vl-modinstlist-weirdint-elim x.modinsts warnings))
    ((mv warnings gateinsts-changedp gateinsts)
     (vl-gateinstlist-weirdint-elim x.gateinsts warnings))
    ((mv warnings alwayses-changedp alwayses)
     (vl-alwayslist-weirdint-elim x.alwayses warnings))
    ((mv warnings initials-changedp initials)
     (vl-initiallist-weirdint-elim x.initials warnings))
    (changedp (or assigns-changedp
                  modinsts-changedp gateinsts-changedp
                  alwayses-changedp initials-changedp))
    ((unless changedp)
     (mv (change-vl-module x :warnings warnings)
         nil))
    (orig-names (vl-exprlist-names (vl-module-allexprs x)))
    ((when (or (member-equal "vl-x-wire" orig-names)
               (member-equal "vl-z-wire" orig-names)))
     (let
      ((warnings
        (fatal
          :type :vl-bad-names
          :msg
          "~m0 already has a wire named \"vl-x-wire\" or \"vl-z-wire\"."
          :args (list (vl-module->name x)))))
      (mv (change-vl-module x :warnings warnings)
          nil)))
    (temp-module (change-vl-module x
                                   :assigns assigns
                                   :modinsts modinsts
                                   :gateinsts gateinsts
                                   :alwayses alwayses
                                   :initials initials
                                   :warnings warnings))
    (new-names (vl-exprlist-names (vl-module-allexprs temp-module)))
    (need-x-wire (member-equal "vl-x-wire" new-names))
    (need-z-wire (member-equal "vl-z-wire" new-names))
    ((unless (or need-x-wire need-z-wire))
     (let
      ((warnings
        (fatal
         :type :vl-weirdint-not-weird
         :msg
         "Expected to at least need X or Z after eliminating weird ints.")))
      (mv (change-vl-module x :warnings warnings)
          nil)))
    (addmods nil)
    (addmods (if need-x-wire (cons *vl-1-bit-x* addmods)
               addmods))
    (addmods (if need-z-wire (cons *vl-1-bit-z* addmods)
               addmods))
    (nf (vl-starting-namefactory temp-module))
    ((mv nf temp-module)
     (if need-x-wire (vl-module-add-x/z-wire nf temp-module :x)
       (mv nf temp-module)))
    ((mv nf temp-module)
     (if need-z-wire (vl-module-add-x/z-wire nf temp-module :z)
       (mv nf temp-module)))
    (- (vl-free-namefactory nf)))
   (mv temp-module addmods))))

Theorem: vl-module-p-of-vl-module-weirdint-elim.new-x

(defthm vl-module-p-of-vl-module-weirdint-elim.new-x
  (b* (((mv ?new-x ?addmods)
        (vl-module-weirdint-elim x)))
    (vl-module-p new-x))
  :rule-classes :rewrite)

Theorem: vl-modulelist-p-of-vl-module-weirdint-elim.addmods

(defthm vl-modulelist-p-of-vl-module-weirdint-elim.addmods
  (b* (((mv ?new-x ?addmods)
        (vl-module-weirdint-elim x)))
    (vl-modulelist-p addmods))
  :rule-classes :rewrite)

Theorem: vl-module-weirdint-elim-mvtypes-1

(defthm vl-module-weirdint-elim-mvtypes-1
  (true-listp (mv-nth 1 (vl-module-weirdint-elim x)))
  :rule-classes :type-prescription)

Theorem: vl-module-weirdint-elim-of-vl-module-fix-x

(defthm vl-module-weirdint-elim-of-vl-module-fix-x
  (equal (vl-module-weirdint-elim (vl-module-fix x))
         (vl-module-weirdint-elim x)))

Theorem: vl-module-weirdint-elim-vl-module-equiv-congruence-on-x

(defthm vl-module-weirdint-elim-vl-module-equiv-congruence-on-x
  (implies (vl-module-equiv x x-equiv)
           (equal (vl-module-weirdint-elim x)
                  (vl-module-weirdint-elim x-equiv)))
  :rule-classes :congruence)