		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-ceq

Generate a wide case-equality module.

Signature
(vl-make-n-bit-ceq n) → mods
Arguments: n — Guard (posp n).
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 module that is written using gates and which is semantically equivalent to:

module VL_N_BIT_CEQ (out, a, b) ;
  output out;
  input [N-1:0] a;
  input [N-1:0] b;
  assign out = (a === b);
endmodule

We basically just instantiate *vl-1-bit-ceq* N times and then reduction-and the results.

Definitions and Theorems

Function: vl-make-n-bit-ceq

(defun vl-make-n-bit-ceq (n)
 (declare (xargs :guard (posp n)))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-make-n-bit-ceq))
   (declare (ignorable __function__))
   (b*
    ((n (lposfix n))
     ((when (eql n 1)) (list *vl-1-bit-ceq*))
     (name (hons-copy (cat "VL_" (natstr n) "_BIT_CEQ")))
     ((mv out-expr
          out-port out-portdecl out-vardecl)
      (vl-occform-mkport "out" :vl-output 1))
     ((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 tmp-expr tmp-vardecl)
      (vl-occform-mkwire "tmp" n))
     (tmp-wires (vl-make-list-of-bitselects tmp-expr 0 (- n 1)))
     (a-wires (vl-make-list-of-bitselects a-expr 0 (- n 1)))
     (b-wires (vl-make-list-of-bitselects b-expr 0 (- n 1)))
     (insts (vl-simple-inst-list *vl-1-bit-ceq*
                                 "bit" tmp-wires a-wires b-wires))
     (and-mods (vl-make-n-bit-reduction-op :vl-unary-bitand n))
     (and-mod (car and-mods))
     (and-inst (vl-simple-inst and-mod "mk_out" out-expr tmp-expr)))
    (list* (make-vl-module
                :name name
                :origname name
                :ports (list out-port a-port b-port)
                :portdecls (list out-portdecl a-portdecl b-portdecl)
                :vardecls (list out-vardecl
                                a-vardecl b-vardecl tmp-vardecl)
                :modinsts (append insts (list and-inst))
                :minloc *vl-fakeloc*
                :maxloc *vl-fakeloc*)
           *vl-1-bit-ceq* and-mods))))

Theorem: vl-modulelist-p-of-vl-make-n-bit-ceq

(defthm vl-modulelist-p-of-vl-make-n-bit-ceq
  (b* ((mods (vl-make-n-bit-ceq n)))
    (vl-modulelist-p mods))
  :rule-classes :rewrite)

Theorem: type-of-vl-make-n-bit-ceq

(defthm type-of-vl-make-n-bit-ceq
  (and (true-listp (vl-make-n-bit-ceq n))
       (consp (vl-make-n-bit-ceq n)))
  :rule-classes :type-prescription)

Theorem: vl-make-n-bit-ceq-of-pos-fix-n

(defthm vl-make-n-bit-ceq-of-pos-fix-n
  (equal (vl-make-n-bit-ceq (pos-fix n))
         (vl-make-n-bit-ceq n)))

Theorem: vl-make-n-bit-ceq-pos-equiv-congruence-on-n

(defthm vl-make-n-bit-ceq-pos-equiv-congruence-on-n
  (implies (acl2::pos-equiv n n-equiv)
           (equal (vl-make-n-bit-ceq n)
                  (vl-make-n-bit-ceq n-equiv)))
  :rule-classes :congruence)