Generate an N-bit latch module for vector-oriented synthesis.
(vl-make-n-bit-latch-vec n del) → mods
We generate basically the following module:
module VL_n_BIT_d_TICK_LATCH (q, clk, d); output [n-1:0] q; input clk; input [n-1:0] d; wire [n-1:0] qdel; wire [n-1:0] qreg; // note: this should be a non-propagating delay, // since any change in qdel is only seen as a change in qreg // and is caused by a change in d or clk that has already propagated. VL_n_BIT_DELAY_1 qdelinst (qdel, qreg); VL_n_BIT_DELAY_d qoutinst (q, qreg); // should be a conservative mux assign qreg = clk ? d : qdel; endmodule
Function:
(defun vl-make-n-bit-latch-vec (n del) (declare (xargs :guard (and (posp n) (natp del)))) (let ((__function__ 'vl-make-n-bit-latch-vec)) (declare (ignorable __function__)) (b* ((n (lposfix n)) (del (lnfix del)) (name (hons-copy (if (zp del) (cat "VL_" (natstr n) "_BIT_LATCH") (cat "VL_" (natstr n) "_BIT_" (natstr del) "_TICK_LATCH")))) ((mv q-expr q-port q-portdecl q-vardecl) (vl-occform-mkport "q" :vl-output n)) ((mv clk-expr clk-port clk-portdecl clk-vardecl) (vl-occform-mkport "clk" :vl-input 1)) ((mv d-expr d-port d-portdecl d-vardecl) (vl-occform-mkport "d" :vl-input n)) ((mv qreg-expr qreg-decls qreg-assigns) (b* (((when (zp del)) (mv q-expr nil nil)) ((mv qregexpr qregdecl) (vl-occform-mkwire "qreg" n)) (ddelassign (make-vl-assign :lvalue q-expr :expr qregexpr :delay (vl-make-constdelay del) :loc *vl-fakeloc*))) (mv qregexpr (list qregdecl) (list ddelassign)))) (triggers (make-vl-nonatom :op :vl-concat :args (list clk-expr d-expr) :finalwidth (+ 1 n) :finaltype :vl-unsigned)) (atts (list (cons "VL_NON_PROP_TRIGGERS" triggers) (cons "VL_NON_PROP_BOUND" qreg-expr) (list "VL_STATE_DELAY"))) ((mv qdel-expr qdel-decl) (vl-occform-mkwire "qdel" n)) (qdel-assign (make-vl-assign :lvalue qdel-expr :expr qreg-expr :delay (vl-make-constdelay 1) :loc *vl-fakeloc* :atts atts)) (qreg-assign (make-vl-assign :lvalue qreg-expr :expr (make-vl-nonatom :op :vl-qmark :args (list clk-expr d-expr qdel-expr) :finalwidth n :finaltype :vl-unsigned :atts (list (list "VL_LATCH_MUX"))) :loc *vl-fakeloc*))) (list (make-vl-module :name name :origname name :ports (list q-port clk-port d-port) :portdecls (list q-portdecl clk-portdecl d-portdecl) :vardecls (list* q-vardecl clk-vardecl d-vardecl qdel-decl qreg-decls) :assigns (list* qreg-assign qdel-assign qreg-assigns) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*)))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-latch-vec (b* ((mods (vl-make-n-bit-latch-vec n del))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-latch-vec (and (true-listp (vl-make-n-bit-latch-vec n del)) (consp (vl-make-n-bit-latch-vec n del))) :rule-classes :type-prescription)