Make an E module to resolve together N inputs into a single output.
(vl-make-n-bit-res-module n) constructs an E module. This models what happens when we drive the same wire with multiple values. There's no notion of strengths here; the wires all have to agree on their value (or be floating) for a good result to come out.
Note that this works even for N=0 (in which case it just always emits Z) and for N=1 (in which case it acts like an ordinary assignment).
Function:
(defun vl-make-n-bit-res-module (n) (declare (xargs :guard (natp n))) (b* ((name (vl-starname (cat "VL_" (natstr n) "_BIT_RES"))) (ins (and (posp n) (vl-emodwires-from-high-to-low "A" (- n 1) 0))) (out (vl-plain-wire-name "O")) (in-pat (and (posp n) (list ins))) (out-pat (list (list out))) (out-alist (list (cons out (vl-make-res-sexpr ins)))) (x (list :out out-alist))) (list :n name :i in-pat :o out-pat :x x)))
Theorem:
(defthm good-esim-primitivep-of-vl-make-n-bit-res-module (implies (natp n) (good-esim-primitivep (vl-make-n-bit-res-module n))))
Theorem:
(defthm good-esim-modulep-of-vl-make-n-bit-res-module (implies (natp n) (good-esim-modulep (vl-make-n-bit-res-module n))))