		Search-engine friendly clone of the ACL2 documentation.

Nedgeflop

Vl-make-1-bit-n-edge-flop

Build the primitive VL module for an n-edge flop.

Signature
(vl-make-1-bit-n-edge-flop n) → flop
Arguments: n — Guard (posp n).
Returns: flop — Type (vl-module-p flop), given the guard.

Definitions and Theorems

Function: vl-make-1-bit-n-edge-flop

(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: vl-module-p-of-vl-make-1-bit-n-edge-flop

(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)