Generate an n-bit wide, 1-tick delay module.
(vl-make-n-bit-delay-1 n &key vecp) → mods
We generate a module in terms of primitives that is equivalent to:
module VL_n_BIT_DELAY_1 (out, in) ; output [n-1:0] out; input [n-1:0] in; assign #1 out = in; endmodule
When
When
module VL_4_BIT_DELAY_1 (out, in) ; output [3:0] out; input [3:0] in; VL_1_BIT_DELAY_1 del0 (out[0], in[0]); VL_1_BIT_DELAY_1 del1 (out[1], in[1]); VL_1_BIT_DELAY_1 del2 (out[2], in[2]); VL_1_BIT_DELAY_1 del3 (out[3], in[3]); endmodule
Function:
(defun vl-make-n-bit-delay-1-fn (n vecp) (declare (xargs :guard (posp n))) (let ((__function__ 'vl-make-n-bit-delay-1)) (declare (ignorable __function__)) (b* (((when (eql n 1)) (list *vl-1-bit-delay-1*)) (name (cat "VL_" (natstr n) "_BIT_DELAY_1")) ((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)) ((when vecp) (b* ((assign (make-vl-assign :lvalue out-expr :expr in-expr :delay (make-vl-gatedelay :rise (vl-make-index 1) :fall (vl-make-index 1)) :loc *vl-fakeloc*)) (mod (make-vl-module :name name :origname name :ports (list out-port in-port) :portdecls (list out-portdecl in-portdecl) :vardecls (list out-vardecl in-vardecl) :assigns (list assign) :minloc *vl-fakeloc* :atts (cons (cons '"VL_SVEX_PRIMITIVE" (make-vl-atom :guts (vl-string "delay"))) (cons (cons '"VL_SVEX_PRIMITIVE_WIDTH" (vl-make-index n)) '(("VL_HANDS_OFF")))) :maxloc *vl-fakeloc*))) (list mod))) (outs (vl-make-list-of-bitselects out-expr 0 (1- n))) (ins (vl-make-list-of-bitselects in-expr 0 (1- n))) (insts (vl-simple-inst-list *vl-1-bit-delay-1* "del" outs ins)) (mod (make-vl-module :name name :origname name :ports (list out-port in-port) :portdecls (list out-portdecl in-portdecl) :vardecls (list out-vardecl in-vardecl) :modinsts insts :minloc *vl-fakeloc* :maxloc *vl-fakeloc*))) (list mod *vl-1-bit-delay-1*))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-delay-1 (implies (and (posp n)) (b* ((mods (vl-make-n-bit-delay-1-fn n vecp))) (vl-modulelist-p mods))) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-delay-1 (and (true-listp (vl-make-n-bit-delay-1 n :vecp vecp)) (consp (vl-make-n-bit-delay-1 n :vecp vecp))) :rule-classes :type-prescription)