Generate a module that propagates Xes from inputs into an answer.
(vl-make-n-bit-x-propagator n m) → mods
We generate a gate-based module that has the following interface:
module VL_N_BY_M_XPROP (out, ans, a, b); output [m-1:0] out; input [m-1:0] ans; input [n-1:0] a; input [n-1:0] b; endmodule
This propagator module can be understood as: if any bit of
Function:
(defun vl-make-n-bit-x-propagator (n m) (declare (xargs :guard (and (posp n) (posp m)))) (declare (xargs :guard t)) (let ((__function__ 'vl-make-n-bit-x-propagator)) (declare (ignorable __function__)) (b* ((n (lposfix n)) (m (lposfix m)) (name (hons-copy (cat "VL_" (natstr n) "_BY_" (natstr m) "_XPROP"))) ((mv out-expr out-port out-portdecl out-vardecl) (vl-occform-mkport "out" :vl-output m)) ((mv ans-expr ans-port ans-portdecl ans-vardecl) (vl-occform-mkport "ans" :vl-input m)) ((mv a-expr a-port a-portdecl a-vardecl) (vl-occform-mkport "a" :vl-input n)) ((mv b-expr b-port b-portdecl b-vardecl) (vl-occform-mkport "b" :vl-input n)) ((mv xdeta-expr xdeta-vardecl) (vl-occform-mkwire "xdet_a" 1)) ((mv xdetb-expr xdetb-vardecl) (vl-occform-mkwire "xdet_b" 1)) ((mv xdet-expr xdet-vardecl) (vl-occform-mkwire "xdet_ab" 1)) ((cons xdet-mod xdet-support) (vl-make-n-bit-xdetect n)) ((cons xeach-mod xeach-support) (vl-make-n-bit-xor-each m)) (xdeta-inst (vl-simple-inst xdet-mod "mk_xdet_a" xdeta-expr a-expr)) (xdetb-inst (vl-simple-inst xdet-mod "mk_xdet_b" xdetb-expr b-expr)) (xdet-inst (vl-simple-inst *vl-1-bit-xor* "mk_xdet_ab" xdet-expr xdeta-expr xdetb-expr)) (xeach-inst (vl-simple-inst xeach-mod "mk_out" out-expr xdet-expr ans-expr))) (list* (make-vl-module :name name :origname name :ports (list out-port ans-port a-port b-port) :portdecls (list out-portdecl ans-portdecl a-portdecl b-portdecl) :vardecls (list out-vardecl ans-vardecl a-vardecl b-vardecl xdeta-vardecl xdetb-vardecl xdet-vardecl) :modinsts (list xdeta-inst xdetb-inst xdet-inst xeach-inst) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) xdet-mod xeach-mod (append xdet-support xeach-support)))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-x-propagator (b* ((mods (vl-make-n-bit-x-propagator n m))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-x-propagator (and (true-listp (vl-make-n-bit-x-propagator n m)) (consp (vl-make-n-bit-x-propagator n m))) :rule-classes :type-prescription)
Theorem:
(defthm vl-make-n-bit-x-propagator-of-pos-fix-n (equal (vl-make-n-bit-x-propagator (pos-fix n) m) (vl-make-n-bit-x-propagator n m)))
Theorem:
(defthm vl-make-n-bit-x-propagator-pos-equiv-congruence-on-n (implies (acl2::pos-equiv n n-equiv) (equal (vl-make-n-bit-x-propagator n m) (vl-make-n-bit-x-propagator n-equiv m))) :rule-classes :congruence)
Theorem:
(defthm vl-make-n-bit-x-propagator-of-pos-fix-m (equal (vl-make-n-bit-x-propagator n (pos-fix m)) (vl-make-n-bit-x-propagator n m)))
Theorem:
(defthm vl-make-n-bit-x-propagator-pos-equiv-congruence-on-m (implies (acl2::pos-equiv m m-equiv) (equal (vl-make-n-bit-x-propagator n m) (vl-make-n-bit-x-propagator n m-equiv))) :rule-classes :congruence)