		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-assign

Generate a wide assignment module.

Signature
(vl-make-n-bit-assign 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 semantically equal to:

module VL_N_BIT_ASSIGN (out, in) ;
  output [n-1:0] out;
  input [n-1:0] in;
  assign out = in;
endmodule

We actually implement these modules using a list of *vl-1-bit-assign* instances, one for each bit. For instance, we implement our four-bit assignment module as:

module VL_4_BIT_ASSIGN (out, in);
  output [3:0] out ;
  input [3:0] in ;
  VL_1_BIT_ASSIGN bit_0 (out[0], in[0]) ;
  VL_1_BIT_ASSIGN bit_1 (out[1], in[1]) ;
  VL_1_BIT_ASSIGN bit_2 (out[2], in[2]) ;
  VL_1_BIT_ASSIGN bit_3 (out[3], in[3]) ;
endmodule

Definitions and Theorems

Function: vl-make-n-bit-assign

(defun vl-make-n-bit-assign (n)
 (declare (xargs :guard (posp n)))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-make-n-bit-assign))
  (declare (ignorable __function__))
  (b* ((n (lposfix n))
       ((when (eql n 1))
        (list *vl-1-bit-assign*))
       (name (hons-copy (cat "VL_" (natstr n) "_BIT_ASSIGN")))
       ((mv out-expr
            out-port out-portdecl out-vardecl)
        (vl-occform-mkport "out" :vl-output n))
       ((mv in-expr in-port in-portdecl in-vardecl)
        (vl-occform-mkport "in" :vl-input n))
       (out-wires (vl-make-list-of-bitselects out-expr 0 (- n 1)))
       (in-wires (vl-make-list-of-bitselects in-expr 0 (- n 1)))
       (modinsts (vl-simple-inst-list *vl-1-bit-assign*
                                      "bit" out-wires in-wires)))
    (list (make-vl-module :name name
                          :origname name
                          :ports (list out-port in-port)
                          :portdecls (list out-portdecl in-portdecl)
                          :vardecls (list out-vardecl in-vardecl)
                          :modinsts modinsts
                          :minloc *vl-fakeloc*
                          :maxloc *vl-fakeloc*)
          *vl-1-bit-assign*))))

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

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

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

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

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

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

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

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