Generate a one-bit wide, M-tick delay module.
(vl-make-1-bit-delay-m m) → mods
We generate a module in terms of primitives that is equivalent to:
module VL_1_BIT_DELAY_M (out, in) ; output out; input in; assign #M out = in; endmodule
When
When
module VL_1_BIT_DELAY_4 (out, in) ; output out; input in; wire [2:0] temp; VL_1_BIT_DELAY_1 del1 (temp[0], in); VL_1_BIT_DELAY_1 del2 (temp[1], temp[0]); VL_1_BIT_DELAY_1 del3 (temp[2], temp[1]); VL_1_BIT_DELAY_1 del4 (out, temp[2]); endmodule
Function:
(defun vl-make-1-bit-delay-m (m) (declare (xargs :guard (posp m))) (let ((__function__ 'vl-make-1-bit-delay-m)) (declare (ignorable __function__)) (b* (((when (eql m 1)) (list *vl-1-bit-delay-1*)) (name (cat "VL_1_BIT_DELAY_" (natstr m))) ((mv out-expr out-port out-portdecl out-vardecl) (vl-occform-mkport "out" :vl-output 1)) ((mv in-expr in-port in-portdecl in-vardecl) (vl-occform-mkport "in" :vl-input 1)) ((mv temp-expr temp-vardecl) (vl-occform-mkwire "temp" (- m 1))) (temp-wires (vl-make-list-of-bitselects temp-expr 0 (- m 2))) (outs (append temp-wires (list out-expr))) (ins (cons in-expr temp-wires)) (insts (vl-make-m-bit-delay-insts 1 "del" (vl-module->name *vl-1-bit-delay-1*) 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 temp-vardecl) :modinsts insts :atts '(("VL_HANDS_OFF")) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*))) (list mod *vl-1-bit-delay-1*))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-1-bit-delay-m (b* ((mods (vl-make-1-bit-delay-m m))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-1-bit-delay-m (and (true-listp (vl-make-1-bit-delay-m m)) (consp (vl-make-1-bit-delay-m m))) :rule-classes :type-prescription)