		Search-engine friendly clone of the ACL2 documentation.

Vl-make-res-occs

Vl-make-n-bit-res-module

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

Definitions and Theorems

Function: vl-make-n-bit-res-module

(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: good-esim-primitivep-of-vl-make-n-bit-res-module

(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: good-esim-modulep-of-vl-make-n-bit-res-module

(defthm good-esim-modulep-of-vl-make-n-bit-res-module
  (implies (natp n)
           (good-esim-modulep (vl-make-n-bit-res-module n))))