Generate a module that shifts an
(vl-make-n-bit-shr-by-m-bits n m) → mods
We generate a gate-based module that is semantically equivalent to:
module VL_N_BIT_SHR_BY_M_BITS (out, a, b) ; output [n-1:0] out; input [n-1:0] a; input [m-1:0] b; assign out = a >> b; endmodule
Function:
(defun vl-make-n-bit-shr-by-m-bits (n m) (declare (xargs :guard (and (posp n) (posp m)))) (declare (xargs :guard t)) (let ((__function__ 'vl-make-n-bit-shr-by-m-bits)) (declare (ignorable __function__)) (b* ((n (lposfix n)) (m (lposfix m)) (name (hons-copy (cat "VL_" (natstr n) "_BIT_SHR_BY_" (natstr m) "_BITS"))) ((mv out-expr out-port out-portdecl out-vardecl) (vl-occform-mkport "out" :vl-output n)) ((mv a-expr a-port a-portdecl a-vardecl) (vl-occform-mkport "a" :vl-input n)) ((mv b-expr b-port b-portdecl b-vardecl) (vl-occform-mkport "b" :vl-input m)) (k (min (+ (integer-length n) 1) m)) ((mv pshift-mods pshift-support) (vl-make-n-bit-shr-place-ps n k)) (pshift-mods (reverse pshift-mods)) (temp-vardecls (reverse (vl-make-list-of-netdecls k "temp" (vl-make-n-bit-range n)))) (temp-exprs (vl-make-idexpr-list (vl-vardecllist->names temp-vardecls) n :vl-unsigned)) (last-temp (car (last temp-exprs))) ((cons xdet-mod xdet-support) (vl-make-n-bit-xdetect m)) ((cons xeach-mod xeach-support) (vl-make-n-bit-xor-each n)) (supporting-mods (list* xdet-mod xeach-mod (append xdet-support xeach-support pshift-mods pshift-support))) ((mv bx-expr bx-vardecl) (vl-occform-mkwire "bx" 1)) (bx-modinst (vl-simple-inst xdet-mod "mk_bx" bx-expr b-expr)) (out-modinst (vl-simple-inst xeach-mod "mk_out" out-expr bx-expr last-temp)) (lhs-exprs (cons a-expr (butlast temp-exprs 1))) (b-wires (vl-make-list-of-bitselects b-expr 0 (- m 1))) ((when (eql m k)) (b* ((pshift-insts (vl-make-modinsts-for-shl 1 pshift-mods temp-exprs lhs-exprs b-wires))) (cons (make-vl-module :name name :origname name :ports (list out-port a-port b-port) :portdecls (list out-portdecl a-portdecl b-portdecl) :vardecls (list* out-vardecl a-vardecl b-vardecl bx-vardecl temp-vardecls) :modinsts (append pshift-insts (list bx-modinst out-modinst)) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) supporting-mods))) (diff (+ 1 (- m k))) ((cons merged-mod merged-support) (vl-make-n-bit-reduction-op :vl-unary-bitor diff)) ((mv merged-expr merged-vardecl) (vl-primitive-mkwire "merged_high")) (high-bits (make-vl-nonatom :op :vl-partselect-colon :args (list b-expr (vl-make-index (- m 1)) (vl-make-index (- k 1))) :finalwidth diff :finaltype :vl-unsigned)) (merged-inst (vl-simple-inst merged-mod "merge_high" merged-expr high-bits)) (lower-wires (take (- k 1) b-wires)) (rhs-exprs (append lower-wires (list merged-expr))) (pshift-insts (vl-make-modinsts-for-shl 1 pshift-mods temp-exprs lhs-exprs rhs-exprs))) (list* (make-vl-module :name name :origname name :ports (list out-port a-port b-port) :portdecls (list out-portdecl a-portdecl b-portdecl) :vardecls (list* out-vardecl a-vardecl b-vardecl bx-vardecl merged-vardecl temp-vardecls) :modinsts (cons merged-inst (append pshift-insts (list bx-modinst out-modinst))) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) merged-mod (append merged-support supporting-mods)))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-shr-by-m-bits (b* ((mods (vl-make-n-bit-shr-by-m-bits n m))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-shr-by-m-bits (and (true-listp (vl-make-n-bit-shr-by-m-bits n m)) (consp (vl-make-n-bit-shr-by-m-bits n m))) :rule-classes :type-prescription)
Theorem:
(defthm vl-make-n-bit-shr-by-m-bits-of-pos-fix-n (equal (vl-make-n-bit-shr-by-m-bits (pos-fix n) m) (vl-make-n-bit-shr-by-m-bits n m)))
Theorem:
(defthm vl-make-n-bit-shr-by-m-bits-pos-equiv-congruence-on-n (implies (acl2::pos-equiv n n-equiv) (equal (vl-make-n-bit-shr-by-m-bits n m) (vl-make-n-bit-shr-by-m-bits n-equiv m))) :rule-classes :congruence)
Theorem:
(defthm vl-make-n-bit-shr-by-m-bits-of-pos-fix-m (equal (vl-make-n-bit-shr-by-m-bits n (pos-fix m)) (vl-make-n-bit-shr-by-m-bits n m)))
Theorem:
(defthm vl-make-n-bit-shr-by-m-bits-pos-equiv-congruence-on-m (implies (acl2::pos-equiv m m-equiv) (equal (vl-make-n-bit-shr-by-m-bits n m) (vl-make-n-bit-shr-by-m-bits n m-equiv))) :rule-classes :congruence)