		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-2^n-bit-dynamic-bitselect

Generates a dynamic bit-selection module for wire widths that are powers of 2.

Signature
(vl-make-2^n-bit-dynamic-bitselect n) → mods
Arguments: n — Guard (natp 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 construct VL_{2^N}_BIT_DYNAMIC_BITSELECT(out, in, idx), a conservative approximation of out = in[idx] where in has width 2^N. We generate this module inductively/recursively by using smaller selectors.

As a basis, when N is 0 or 1, we use the 1-bit or 2-bit selectors that we pre-define; see *vl-1-bit-dynamic-bitselect* and *vl-2-bit-dynamic-bitselect*.

When N > 1, let M be 2^N and K be 2^(N-1). We define VL_M_BIT_DYNAMIC_BITSELECT in Verilog as follows:

module VL_M_BIT_DYNAMIC_BITSELECT(out, in, idx) ;

   output out;
   input [M-1:0] in;
   input [N-1:0] idx;

   wire high; // result assuming idx[N-1] is high
   wire low;  // result assuming idx[N-1] is low

   VL_K_BIT_DYNAMIC_BITSELECT mk_high (high, in[M-1:K], idx[N-2:0]);
   VL_K_BIT_DYNAMIC_BITSELECT mk_low  (low,  in[K-1:0], idx[N-2:0]);

   // Choose high or low, per idx[N-1]

   wire idx_bar;
   wire a;
   wire b;
   wire main;

   not (idx_bar, idx[N-1]);
   and (a, idx[N-1], high) ;
   and (b, idx_bar, low) ;
   or  (main, a, b) ;

   // Fix up main so that if idx[N-1] is X we produce X.

   wire idx_x;
   xor (idx_x, idx[N-1], idx[N-1]);
   xor (out, idx_x, main);

endmodule

Definitions and Theorems

Function: vl-make-2^n-bit-dynamic-bitselect

(defun vl-make-2^n-bit-dynamic-bitselect (n)
 (declare (xargs :guard (natp n)))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-make-2^n-bit-dynamic-bitselect))
  (declare (ignorable __function__))
  (b*
   (((when (zp n))
     (list *vl-1-bit-dynamic-bitselect*))
    ((when (eql n 1))
     (list *vl-2-bit-dynamic-bitselect*))
    (m (expt 2 n))
    (k (expt 2 (1- n)))
    (submods (vl-make-2^n-bit-dynamic-bitselect (- n 1)))
    (name (hons-copy (cat "VL_" (natstr m)
                          "_BIT_DYNAMIC_BITSELECT")))
    ((mv out-expr
         out-port out-portdecl out-vardecl)
     (vl-primitive-mkport "out" :vl-output))
    ((mv in-expr in-port in-portdecl in-vardecl)
     (vl-occform-mkport "in" :vl-input m))
    ((mv idx-expr
         idx-port idx-portdecl idx-vardecl)
     (vl-occform-mkport "idx" :vl-input n))
    ((mv high-expr high-vardecl)
     (vl-primitive-mkwire "high"))
    ((mv low-expr low-vardecl)
     (vl-primitive-mkwire "low"))
    ((mv ~idx-expr ~idx-vardecl)
     (vl-primitive-mkwire "idx_bar"))
    ((mv a-expr a-vardecl)
     (vl-primitive-mkwire "a"))
    ((mv b-expr b-vardecl)
     (vl-primitive-mkwire "b"))
    ((mv main-expr main-vardecl)
     (vl-primitive-mkwire "main"))
    ((mv idx_x-expr idx_x-vardecl)
     (vl-primitive-mkwire "idx_x"))
    (|in[m-1]:k| (vl-make-partselect in-expr (- m 1) k))
    (|in[k-1:0]| (vl-make-partselect in-expr (- k 1) 0))
    (idx[n-1] (vl-make-bitselect idx-expr (- n 1)))
    (|idx[n-2:0]| (vl-make-partselect idx-expr (- n 2) 0))
    (high-inst (vl-simple-inst (car submods)
                               "mk_high"
                               high-expr |in[m-1]:k| |idx[n-2:0]|))
    (low-inst (vl-simple-inst (car submods)
                              "mk_low"
                              low-expr |in[k-1:0]| |idx[n-2:0]|))
    (~idx-inst (vl-simple-inst *vl-1-bit-not*
                               "mk_idx_bar" ~idx-expr idx[n-1]))
    (a-inst (vl-simple-inst *vl-1-bit-and*
                            "mk_a" a-expr idx[n-1] high-expr))
    (b-inst (vl-simple-inst *vl-1-bit-and*
                            "mk_b" b-expr ~idx-expr low-expr))
    (main-inst (vl-simple-inst *vl-1-bit-or*
                               "mk_main" main-expr a-expr b-expr))
    (idx_x-inst (vl-simple-inst *vl-1-bit-xor* "mk_idx_x"
                                idx_x-expr idx[n-1] idx[n-1]))
    (out-inst (vl-simple-inst *vl-1-bit-xor* "mk_out"
                              out-expr idx_x-expr main-expr)))
   (list*
        (make-vl-module
             :name name
             :origname name
             :ports (list out-port in-port idx-port)
             :portdecls (list out-portdecl in-portdecl idx-portdecl)
             :vardecls (list out-vardecl
                             in-vardecl idx-vardecl high-vardecl
                             low-vardecl ~idx-vardecl a-vardecl
                             b-vardecl main-vardecl idx_x-vardecl)
             :modinsts (list high-inst low-inst ~idx-inst a-inst
                             b-inst main-inst idx_x-inst out-inst)
             :minloc *vl-fakeloc*
             :maxloc *vl-fakeloc*)
        *vl-1-bit-not* *vl-1-bit-and*
        *vl-1-bit-or* *vl-1-bit-xor* submods))))

Theorem: vl-modulelist-p-of-vl-make-2^n-bit-dynamic-bitselect

(defthm vl-modulelist-p-of-vl-make-2^n-bit-dynamic-bitselect
  (b* ((mods (vl-make-2^n-bit-dynamic-bitselect n)))
    (vl-modulelist-p mods))
  :rule-classes :rewrite)

Theorem: type-of-vl-make-2^n-bit-dynamic-bitselect

(defthm type-of-vl-make-2^n-bit-dynamic-bitselect
  (and (true-listp (vl-make-2^n-bit-dynamic-bitselect n))
       (consp (vl-make-2^n-bit-dynamic-bitselect n)))
  :rule-classes :type-prescription)

Theorem: vl-make-2^n-bit-dynamic-bitselect-of-nfix-n

(defthm vl-make-2^n-bit-dynamic-bitselect-of-nfix-n
  (equal (vl-make-2^n-bit-dynamic-bitselect (nfix n))
         (vl-make-2^n-bit-dynamic-bitselect n)))

Theorem: vl-make-2^n-bit-dynamic-bitselect-nat-equiv-congruence-on-n

(defthm vl-make-2^n-bit-dynamic-bitselect-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (vl-make-2^n-bit-dynamic-bitselect n)
                  (vl-make-2^n-bit-dynamic-bitselect n-equiv)))
  :rule-classes :congruence)