		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-nedgeflop

Generate an N-bit register with K edges.

Signature
(vl-make-nedgeflop width nedges) → mods
Returns: mods — A non-empty module list. The first module in the list is the desired module; the other modules are any necessary supporting modules.
Type (vl-modulelist-p mods).

Definitions and Theorems

Function: vl-make-nedgeflop

(defun vl-make-nedgeflop (width nedges)
 (declare (xargs :guard (and (posp width) (posp nedges))))
 (let ((__function__ 'vl-make-nedgeflop))
   (declare (ignorable __function__))
   (b*
    ((width (lposfix width))
     (nedges (lposfix nedges))
     ((when (eql width 1))
      (list (vl-make-1-bit-n-edge-flop nedges)))
     (name (cat "VL_" (natstr width)
                "_BIT_" (natstr nedges)
                "_EDGE_FLOP"))
     ((mv q-expr q-port q-portdecl q-vardecl)
      (vl-occform-mkport "q"
                         :vl-output width))
     ((mv d-exprs d-ports d-portdecls d-vardecls)
      (vl-occform-mkports "d" 0 nedges
                          :dir :vl-input
                          :width width))
     ((mv clk-exprs
          clk-ports clk-portdecls clk-vardecls)
      (vl-occform-mkports "clk" 0 nedges
                          :dir :vl-input
                          :width 1))
     (primitive (vl-make-1-bit-n-edge-flop nedges))
     (modinsts
          (vl-make-nedgeflop-insts primitive
                                   q-expr d-exprs clk-exprs width)))
    (list (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))
               :modinsts modinsts
               :minloc *vl-fakeloc*
               :maxloc *vl-fakeloc*)
          primitive))))

Theorem: vl-modulelist-p-of-vl-make-nedgeflop

(defthm vl-modulelist-p-of-vl-make-nedgeflop
  (b* ((mods (vl-make-nedgeflop width nedges)))
    (vl-modulelist-p mods))
  :rule-classes :rewrite)

Theorem: type-of-vl-make-nedgeflop

(defthm type-of-vl-make-nedgeflop
  (and (true-listp (vl-make-nedgeflop width nedges))
       (consp (vl-make-nedgeflop width nedges)))
  :rule-classes :type-prescription)