		Search-engine friendly clone of the ACL2 documentation.

Weirdint-elim

Vl-module-add-x/z-wire

Extend mod with a wire declaration for vl-x-wire or vl-z-wire, and a module instance that drives it.

Signature
(vl-module-add-x/z-wire nf mod which) → (mv nf new-mod)
Arguments: nf — Guard (vl-namefactory-p nf).; mod — Guard (vl-module-p mod).; which — Guard (or (eq which :x) (eq which :z)).
Returns: nf — Type (vl-namefactory-p nf).; new-mod — Type (vl-module-p new-mod).

Definitions and Theorems

Function: vl-module-add-x/z-wire

(defun vl-module-add-x/z-wire (nf mod which)
 (declare (xargs :guard (and (vl-namefactory-p nf)
                             (vl-module-p mod)
                             (or (eq which :x) (eq which :z)))))
 (let ((__function__ 'vl-module-add-x/z-wire))
   (declare (ignorable __function__))
   (b*
    ((vardecls (vl-module->vardecls mod))
     (modinsts (vl-module->modinsts mod))
     (wirename (if (eq which :x)
                   "vl-x-wire"
                 "vl-z-wire"))
     ((mv instname nf)
      (vl-namefactory-plain-name (if (eq which :x)
                                     "vl_make_x_wire"
                                   "vl_make_z_wire")
                                 nf))
     (target-mod (if (eq which :x)
                     *vl-1-bit-x*
                   *vl-1-bit-z*))
     (new-vardecl (make-vl-vardecl :name wirename
                                   :type *vl-plain-old-wire-type*
                                   :nettype :vl-wire
                                   :loc *vl-fakeloc*))
     (new-expr (if (eq which :x)
                   *vl-x-wire-expr*
                 *vl-z-wire-expr*))
     (new-modinst
          (make-vl-modinst
               :modname (vl-module->name target-mod)
               :instname instname
               :paramargs (make-vl-paramargs-plain :args nil)
               :portargs
               (make-vl-arguments-plain
                    :args (list (make-vl-plainarg :expr new-expr
                                                  :dir :vl-output
                                                  :portname "out")))
               :loc *vl-fakeloc*))
     (mod-prime
          (change-vl-module mod
                            :vardecls (cons new-vardecl vardecls)
                            :modinsts (cons new-modinst modinsts))))
    (mv nf mod-prime))))

Theorem: vl-namefactory-p-of-vl-module-add-x/z-wire.nf

(defthm vl-namefactory-p-of-vl-module-add-x/z-wire.nf
  (b* (((mv ?nf ?new-mod)
        (vl-module-add-x/z-wire nf mod which)))
    (vl-namefactory-p nf))
  :rule-classes :rewrite)

Theorem: vl-module-p-of-vl-module-add-x/z-wire.new-mod

(defthm vl-module-p-of-vl-module-add-x/z-wire.new-mod
  (b* (((mv ?nf ?new-mod)
        (vl-module-add-x/z-wire nf mod which)))
    (vl-module-p new-mod))
  :rule-classes :rewrite)

Theorem: vl-module-add-x/z-wire-of-vl-namefactory-fix-nf

(defthm vl-module-add-x/z-wire-of-vl-namefactory-fix-nf
  (equal (vl-module-add-x/z-wire (vl-namefactory-fix nf)
                                 mod which)
         (vl-module-add-x/z-wire nf mod which)))

Theorem: vl-module-add-x/z-wire-vl-namefactory-equiv-congruence-on-nf

(defthm vl-module-add-x/z-wire-vl-namefactory-equiv-congruence-on-nf
  (implies (vl-namefactory-equiv nf nf-equiv)
           (equal (vl-module-add-x/z-wire nf mod which)
                  (vl-module-add-x/z-wire nf-equiv mod which)))
  :rule-classes :congruence)

Theorem: vl-module-add-x/z-wire-of-vl-module-fix-mod

(defthm vl-module-add-x/z-wire-of-vl-module-fix-mod
  (equal (vl-module-add-x/z-wire nf (vl-module-fix mod)
                                 which)
         (vl-module-add-x/z-wire nf mod which)))

Theorem: vl-module-add-x/z-wire-vl-module-equiv-congruence-on-mod

(defthm vl-module-add-x/z-wire-vl-module-equiv-congruence-on-mod
  (implies (vl-module-equiv mod mod-equiv)
           (equal (vl-module-add-x/z-wire nf mod which)
                  (vl-module-add-x/z-wire nf mod-equiv which)))
  :rule-classes :congruence)