Extend mod with a wire declaration for vl-x-wire or vl-z-wire, and a module instance that drives it.
(vl-module-add-x/z-wire nf mod which) → (mv nf new-mod)
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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)