Generate an N-bit wide, M-tick delay module.
(vl-make-n-bit-delay-m n m &key vecp) → mods
We generate a module in terms of primitives that is equivalent to:
module VL_N_BIT_DELAY_M (out, in) ; output [N-1:0] out; input [N-1:0] in; assign #M out = in; endmodule
In the special case that
Otherwise, we just chain together a list of these modules, one for each tick. For instance, a module that implements 4-bit wide delay for 3 ticks would look like this:
module VL_4_BIT_DELAY_3 (out, in); output [3:0] out; output [3:0] in; wire [3:0] temp1; wire [3:0] temp2; VL_4_BIT_DELAY_1 bit0 (temp1, in); VL_4_BIT_DELAY_1 bit1 (temp2, temp1); VL_4_BIT_DELAY_1 bit2 (out, temp2); endmodule
Function:
(defun vl-make-n-bit-delay-m-fn (n m vecp) (declare (xargs :guard (and (posp n) (posp m)))) (let ((__function__ 'vl-make-n-bit-delay-m)) (declare (ignorable __function__)) (b* ((base (vl-make-n-bit-delay-1 n :vecp vecp)) ((when (= m 1)) base) (name (cat "VL_" (natstr n) "_BIT_DELAY_" (natstr m))) ((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 tmp-exprs tmp-vardecls) (vl-occform-mkwires "temp" 1 m :width n)) (outs (append tmp-exprs (list out-expr))) (ins (cons in-expr tmp-exprs)) (insts (vl-simple-inst-list (car base) "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 tmp-vardecls) :modinsts insts :minloc *vl-fakeloc* :maxloc *vl-fakeloc*))) (cons mod base))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-delay-m (implies (and (posp n) (posp m)) (b* ((mods (vl-make-n-bit-delay-m-fn n m vecp))) (vl-modulelist-p mods))) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-delay-m (and (true-listp (vl-make-n-bit-delay-m n m :vecp vecp)) (consp (vl-make-n-bit-delay-m n m :vecp vecp))) :rule-classes :type-prescription)