		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-dynamic-bitselect

Generate a basic dynamic bit-selection module.

Signature
(vl-make-n-bit-dynamic-bitselect 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 construct VL_N_BIT_DYNAMIC_BITSELECT(out, in, idx), a conservative approximation of out = in[idx] where in has width N and idx has the minimum width necessary to select from N bits. In particular, the width of idx is the smallest number W such that N <= 2^W.

When N is a power of 2, we simply construct the desired module using vl-make-2^n-bit-dynamic-bitselect.

Otherwise, the basic strategy is to instantiate the next biggest power of 2, and then pad in with however many X bits are necessary to obtain an input of this larger size. As an example, we implement a 6-bit select by using an 8-bit select as follows:

module VL_6_BIT_DYNAMIC_BITSELECT(out, in, idx) ;

   output out;
   input [5:0] in;
   input [2:0] idx;

   VL_8_BIT_DYNAMIC_BITSELECT core(out, {2'bxx, in}, idx);

endmodule

Definitions and Theorems

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

(defun vl-make-n-bit-dynamic-bitselect (n)
 (declare (xargs :guard (posp n)))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-make-n-bit-dynamic-bitselect))
  (declare (ignorable __function__))
  (b*
   ((n (lposfix n))
    (bitlength (next-power-of-2 n))
    (2^bitlength (expt 2 bitlength))
    (coremods (vl-make-2^n-bit-dynamic-bitselect bitlength))
    ((when (eql 2^bitlength n)) coremods)
    (name (hons-copy (cat "VL_" (natstr n)
                          "_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 n))
    ((mv idx-expr
         idx-port idx-portdecl idx-vardecl)
     (vl-occform-mkport "idx"
                        :vl-input bitlength))
    (padlen (- 2^bitlength n))
    (|padlen'bxxx|
      (make-vl-atom
           :guts (make-vl-weirdint :bits (replicate padlen :vl-xval)
                                   :origwidth padlen
                                   :origtype :vl-unsigned)
           :finalwidth padlen
           :finaltype :vl-unsigned))
    (pad-expr (make-vl-nonatom :op :vl-concat
                               :args (list |padlen'bxxx| in-expr)
                               :finalwidth 2^bitlength
                               :finaltype :vl-unsigned))
    (inst (vl-simple-inst (car coremods)
                          "core" out-expr pad-expr idx-expr)))
   (cons
        (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)
             :modinsts (list inst)
             :minloc *vl-fakeloc*
             :maxloc *vl-fakeloc*)
        coremods))))

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

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

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

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

Theorem: vl-make-n-bit-dynamic-bitselect-of-pos-fix-n

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

Theorem: vl-make-n-bit-dynamic-bitselect-pos-equiv-congruence-on-n

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