Generate a basic dynamic bit-selection module.
(vl-make-n-bit-dynamic-bitselect n) → mods
We construct
When
Otherwise, the basic strategy is to instantiate the next biggest power of 2,
and then pad
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
Function:
(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:
(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:
(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:
(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:
(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)