		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-x-propagator

Generate a module that propagates Xes from inputs into an answer.

Signature
(vl-make-n-bit-x-propagator n m) → mods
Arguments: n — Guard (posp n).; m — Guard (posp m).
Returns: mods — A non-empty module list. The first module in the list is the desired module; the other modules are any necessary supporting modules.
Type (vl-modulelist-p 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 a or b is X/Z, then out will be all X bits. Otherwise out is just a copy of ans.

Definitions and Theorems

Function: vl-make-n-bit-x-propagator

(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: vl-modulelist-p-of-vl-make-n-bit-x-propagator

(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: type-of-vl-make-n-bit-x-propagator

(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: vl-make-n-bit-x-propagator-of-pos-fix-n

(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: vl-make-n-bit-x-propagator-pos-equiv-congruence-on-n

(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: vl-make-n-bit-x-propagator-of-pos-fix-m

(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: vl-make-n-bit-x-propagator-pos-equiv-congruence-on-m

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