Generates a dynamic bit-selection module for wire widths that are powers of 2.
(vl-make-2^n-bit-dynamic-bitselect n) → mods
We construct
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
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
Function:
(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:
(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:
(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:
(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:
(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)