		Search-engine friendly clone of the ACL2 documentation.

Vl-make-res-occs

Vl-make-res-occ

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 out to all of the values on ins.

Definitions and Theorems

Function: vl-make-res-occ

(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: good-esim-occp-of-vl-make-res-occ

(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))))