Generate a module that conditionally shifts an
(vl-make-n-bit-shr-place-p n p) → mods
We generate a gate-based module that is semantically equivalent to:
module VL_N_BIT_SHR_PLACE_P (out, in, shiftp) ; output [n-1:0] out; input [n-1:0] in; input shiftp; assign out = shiftp ? (in >> 2**(p-1)) : in; endmodule
These "place shifters" can be combined to form a full shifter that operates on O(log_2 n) muxes.
Function:
(defun vl-make-n-bit-shr-place-p (n p) (declare (xargs :guard (and (posp n) (posp p)))) (declare (xargs :guard t)) (let ((__function__ 'vl-make-n-bit-shr-place-p)) (declare (ignorable __function__)) (b* ((n (lposfix n)) (p (lposfix p)) (shift-amount (expt 2 (- p 1))) (name (hons-copy (cat "VL_" (natstr n) "_BIT_SHR_PLACE_" (natstr p)))) ((mv out-expr out-port out-portdecl out-vardecl) (vl-occform-mkport "out" :vl-output n)) ((mv in-expr in-port in-portdecl in-vardecl) (vl-occform-mkport "in" :vl-input n)) ((mv shiftp-expr shiftp-port shiftp-portdecl shiftp-vardecl) (vl-primitive-mkport "shiftp" :vl-input)) (places (min n shift-amount)) (|places'b0| (make-vl-atom :guts (make-vl-constint :value 0 :origwidth places :origtype :vl-unsigned) :finalwidth places :finaltype :vl-unsigned)) (shifted-expr (if (<= n shift-amount) |places'b0| (make-vl-nonatom :op :vl-concat :args (list |places'b0| (vl-make-partselect in-expr (- n 1) places)) :finalwidth n :finaltype :vl-unsigned))) ((cons mux-mod mux-support) (vl-make-n-bit-mux n t)) (mux-inst (vl-simple-inst mux-mod "mux" out-expr shiftp-expr shifted-expr in-expr))) (list* (make-vl-module :name name :origname name :ports (list out-port in-port shiftp-port) :portdecls (list out-portdecl in-portdecl shiftp-portdecl) :vardecls (list out-vardecl in-vardecl shiftp-vardecl) :modinsts (list mux-inst) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) mux-mod mux-support))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-shr-place-p (b* ((mods (vl-make-n-bit-shr-place-p n p))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-shr-place-p (and (true-listp (vl-make-n-bit-shr-place-p n p)) (consp (vl-make-n-bit-shr-place-p n p))) :rule-classes :type-prescription)
Theorem:
(defthm vl-make-n-bit-shr-place-p-of-pos-fix-n (equal (vl-make-n-bit-shr-place-p (pos-fix n) p) (vl-make-n-bit-shr-place-p n p)))
Theorem:
(defthm vl-make-n-bit-shr-place-p-pos-equiv-congruence-on-n (implies (acl2::pos-equiv n n-equiv) (equal (vl-make-n-bit-shr-place-p n p) (vl-make-n-bit-shr-place-p n-equiv p))) :rule-classes :congruence)
Theorem:
(defthm vl-make-n-bit-shr-place-p-of-pos-fix-p (equal (vl-make-n-bit-shr-place-p n (pos-fix p)) (vl-make-n-bit-shr-place-p n p)))
Theorem:
(defthm vl-make-n-bit-shr-place-p-pos-equiv-congruence-on-p (implies (acl2::pos-equiv p p-equiv) (equal (vl-make-n-bit-shr-place-p n p) (vl-make-n-bit-shr-place-p n p-equiv))) :rule-classes :congruence)