Build the primitive VL module for an n-edge flop.
(vl-make-1-bit-n-edge-flop n) → flop
Function:
(defun vl-make-1-bit-n-edge-flop (n) (declare (xargs :guard (posp n))) (let ((__function__ 'vl-make-1-bit-n-edge-flop)) (declare (ignorable __function__)) (b* ((name (cat "VL_1_BIT_" (natstr n) "_EDGE_FLOP")) ((mv q-expr q-port q-portdecl q-vardecl) (vl-primitive-mkport "q" :vl-output)) (q-portdecl (change-vl-portdecl q-portdecl :type *vl-plain-old-reg-type*)) (q-vardecl (change-vl-vardecl q-vardecl :type *vl-plain-old-reg-type*)) ((mv d-exprs d-ports d-portdecls d-vardecls) (vl-primitive-mkports "d" 0 n :dir :vl-input)) ((mv clk-exprs clk-ports clk-portdecls clk-vardecls) (vl-primitive-mkports "clk" 0 n :dir :vl-input)) (always (vl-nedgeflop-always q-expr clk-exprs d-exprs)) (temp-mod (make-vl-module :name name :origname name :ports (cons q-port (append d-ports clk-ports)) :portdecls (cons q-portdecl (append d-portdecls clk-portdecls)) :vardecls (cons q-vardecl (append d-vardecls clk-vardecls)) :alwayses (list always) :minloc *vl-fakeloc* :maxloc *vl-fakeloc* :atts (list (cons (hons-copy "VL_HANDS_OFF") nil)))) ((mv okp warnings walist) (vl-module-wirealist temp-mod nil)) ((unless (and okp (not warnings))) (raise "Error creating wire alist? ~s0" (vl-warnings-to-string warnings)) temp-mod) (q-wire (car (vl-nedgeflop-e-wires (list q-expr) walist))) (d-wires (vl-nedgeflop-e-wires d-exprs walist)) (clk-wires (vl-nedgeflop-e-wires clk-exprs walist)) (q-prev (car (vl-emodwires-from-msb-to-lsb "q_prev" 0 0))) (d-prevs (vl-emodwires-from-msb-to-lsb "d_prev" (- n 1) 0)) (clk-prevs (vl-emodwires-from-msb-to-lsb "clk_prev" (- n 1) 0)) (next-q-sexpr (acl2::4vs-ite*-dumb (vl-nedgeflop-some-edge-sexpr clk-wires clk-prevs) (vl-nedgeflop-update-sexpr clk-wires d-prevs) q-prev)) (nst-alist (cons (cons q-prev next-q-sexpr) (append (pairlis$ clk-prevs clk-wires) (pairlis$ d-prevs d-wires)))) (out-alist (list (cons q-wire next-q-sexpr))) (esim (list :n (vl-starname name) :o (list (list q-wire)) :i (append (pairlis$ d-wires nil) (pairlis$ clk-wires nil)) :x (list :out out-alist :nst nst-alist) :a (list (cons "VL_N_EDGE_FLOP" t) (cons "VL_FLOP_NUM_EDGES" n) (cons "VL_FLOP_CLK_WIRES" clk-wires) (cons "VL_FLOP_CLK_PREVS" clk-prevs) (cons "VL_FLOP_D_WIRES" d-wires) (cons "VL_FLOP_D_PREVS" d-prevs) (cons "VL_FLOP_Q_WIRE" q-wire) (cons "VL_FLOP_Q_PREV" q-prev))))) (change-vl-module temp-mod :esim esim))))
Theorem:
(defthm vl-module-p-of-vl-make-1-bit-n-edge-flop (implies (and (force (posp n))) (b* ((flop (vl-make-1-bit-n-edge-flop n))) (vl-module-p flop))) :rule-classes :rewrite)