Generate a dynamic bit-selection module for an N bit wire and an M bit select.
(vl-make-n-bit-dynamic-bitselect-m n m) → mods
We produce
Prerequisite: see vl-make-n-bit-dynamic-bitselect, which can be used
to introduce a module
The problem with just using
Function:
(defun vl-make-n-bit-dynamic-bitselect-m (n m) (declare (xargs :guard (and (posp n) (posp m)))) (declare (xargs :guard t)) (let ((__function__ 'vl-make-n-bit-dynamic-bitselect-m)) (declare (ignorable __function__)) (b* ((n (lposfix n)) (m (lposfix m)) (coremods (vl-make-n-bit-dynamic-bitselect n)) (coremod (car coremods)) (k (b* ((portdecls (vl-module->portdecls coremod)) (idx (vl-find-portdecl "idx" portdecls)) ((unless idx) (raise "coremod has no index port?") m) (type (vl-portdecl->type idx)) ((unless (eq (vl-datatype-kind type) :vl-coretype)) (raise "coremod port isn't a coretype?") m) ((vl-coretype type)) ((unless (and (atom type.udims) (or (atom type.pdims) (and (atom (cdr type.pdims)) (not (eq (car type.pdims) :vl-unsized-dimension)))))) (raise "coremod index unexpected array dims") m) (range (and (consp type.pdims) (car type.pdims))) ((unless (vl-maybe-range-resolved-p range)) (raise "coremod index range not resolved?") m)) (vl-maybe-range-size range))) ((when (eql k m)) coremods) (name (cat "VL_" (natstr n) "_BIT_DYNAMIC_BITSELECT_" (natstr m))) ((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 m)) ((when (< k m)) (b* ((lowbits (vl-make-partselect idx-expr (- k 1) 0)) (highbits (vl-make-partselect idx-expr (- m 1) k)) ((mv main-expr main-vardecl) (vl-primitive-mkwire "main")) (core-inst (vl-simple-inst (car coremods) "core" main-expr in-expr lowbits)) ((cons extra-mod extra-support) (vl-make-n-bit-reduction-op :vl-unary-bitor (- m k))) ((mv extra-expr extra-vardecl) (vl-primitive-mkwire "any_extra")) (extra-inst (vl-simple-inst extra-mod "mk_any_extra" extra-expr highbits)) ((mv noextra-expr noextra-vardecl) (vl-primitive-mkwire "no_extra")) ((mv a-expr a-vardecl) (vl-primitive-mkwire "a")) ((mv b-expr b-vardecl) (vl-primitive-mkwire "b")) (noextra-inst (vl-simple-inst *vl-1-bit-not* "mk_no_extra" noextra-expr extra-expr)) (a-inst (vl-simple-inst *vl-1-bit-and* "mk_a" a-expr noextra-expr main-expr)) (b-inst (vl-simple-inst *vl-1-bit-and* "mk_b" b-expr extra-expr |*sized-1'bx*|)) (out-inst (vl-simple-inst *vl-1-bit-or* "mk_out" out-expr a-expr b-expr)) (mod (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 main-vardecl extra-vardecl noextra-vardecl a-vardecl b-vardecl) :modinsts (list core-inst extra-inst noextra-inst a-inst b-inst out-inst) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*))) (list* mod extra-mod (append coremods extra-support)))) (padsize (- k m)) (pad-expr (make-vl-atom :guts (make-vl-constint :value 0 :origwidth padsize :origtype :vl-unsigned) :finalwidth padsize :finaltype :vl-unsigned)) (padded-idx (make-vl-nonatom :op :vl-concat :args (list pad-expr idx-expr) :finalwidth k :finaltype :vl-unsigned)) (core-inst (vl-simple-inst (car coremods) "core" out-expr in-expr padded-idx))) (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) :modinsts (list core-inst) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) *vl-1-bit-not* *vl-1-bit-and* *vl-1-bit-or* coremods))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-dynamic-bitselect-m (b* ((mods (vl-make-n-bit-dynamic-bitselect-m n m))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-dynamic-bitselect-m (and (true-listp (vl-make-n-bit-dynamic-bitselect-m n m)) (consp (vl-make-n-bit-dynamic-bitselect-m n m))) :rule-classes :type-prescription)
Theorem:
(defthm vl-make-n-bit-dynamic-bitselect-m-of-pos-fix-n (equal (vl-make-n-bit-dynamic-bitselect-m (pos-fix n) m) (vl-make-n-bit-dynamic-bitselect-m n m)))
Theorem:
(defthm vl-make-n-bit-dynamic-bitselect-m-pos-equiv-congruence-on-n (implies (acl2::pos-equiv n n-equiv) (equal (vl-make-n-bit-dynamic-bitselect-m n m) (vl-make-n-bit-dynamic-bitselect-m n-equiv m))) :rule-classes :congruence)
Theorem:
(defthm vl-make-n-bit-dynamic-bitselect-m-of-pos-fix-m (equal (vl-make-n-bit-dynamic-bitselect-m n (pos-fix m)) (vl-make-n-bit-dynamic-bitselect-m n m)))
Theorem:
(defthm vl-make-n-bit-dynamic-bitselect-m-pos-equiv-congruence-on-m (implies (acl2::pos-equiv m m-equiv) (equal (vl-make-n-bit-dynamic-bitselect-m n m) (vl-make-n-bit-dynamic-bitselect-m n m-equiv))) :rule-classes :congruence)