Generate and instantiate an appropriate resolution module to drive a wire to multiple values.
(vl-make-res-occ name out ins) builds an E occurrence that simultaneously
drives
Function:
(defun vl-make-res-occ (name out ins) (declare (xargs :guard (and (vl-emodwire-p out) (vl-emodwirelist-p ins) (true-listp ins) (uniquep ins)))) (b* ((n (len ins)) (op (vl-make-n-bit-res-module n)) (i (and (posp n) (list ins))) (o (list (list out)))) (list :u name :op op :i i :o o)))
Theorem:
(defthm good-esim-occp-of-vl-make-res-occ (implies (and (force (vl-emodwire-p out)) (force (vl-emodwirelist-p ins)) (force (true-listp ins)) (force (uniquep ins)) (force name)) (good-esim-occp (vl-make-res-occ name out ins))))