		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-nedgeflop-vec

Generate a w-bit wide, n-edge flop with output delay d

Signature
(vl-make-nedgeflop-vec width nedges delay) → 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-vec

(defun vl-make-nedgeflop-vec (width nedges delay)
 (declare (xargs :guard (and (posp width)
                             (posp nedges)
                             (natp delay))))
 (let ((__function__ 'vl-make-nedgeflop-vec))
  (declare (ignorable __function__))
  (b*
   ((width (lposfix width))
    (nedges (lposfix nedges))
    (delay (lnfix delay))
    (name (if (zp delay)
              (cat "VL_" (natstr width)
                   "_BIT_" (natstr nedges)
                   "_EDGE_FLOP")
            (cat "VL_" (natstr width)
                 "_BIT_" (natstr nedges)
                 "_EDGE_" (natstr delay)
                 "_TICK_FLOP")))
    ((mv qexpr qport qportdecl qvardecl)
     (vl-occform-mkport "q"
                        :vl-output width))
    ((mv dexprs dports dportdecls dvardecls)
     (vl-occform-mkports "d" 0 nedges
                         :dir :vl-input
                         :width width))
    ((mv clkexprs
         clkports clkportdecls clkvardecls)
     (vl-occform-mkports "clk" 0 nedges
                         :dir :vl-input
                         :width 1))
    ((mv qregexpr qregdecls qregassigns)
     (b*
      (((when (zp delay)) (mv qexpr nil nil))
       ((mv qregexpr qregdecl)
        (vl-occform-mkwire "qreg" width))
       (ddelassign (make-vl-assign :lvalue qexpr
                                   :expr qregexpr
                                   :delay (vl-make-constdelay delay)
                                   :loc *vl-fakeloc*)))
      (mv qregexpr (list qregdecl)
          (list ddelassign))))
    (clkconcat (make-vl-nonatom :op :vl-concat
                                :args clkexprs
                                :finalwidth nedges
                                :finaltype :vl-unsigned))
    (atts (list (cons "VL_NON_PROP_TRIGGERS" clkconcat)
                (cons "VL_NON_PROP_BOUND" qregexpr)
                (list "VL_STATE_DELAY")))
    ((mv clkdelexprs clkdeldecls)
     (vl-occform-mkwires "clkdel" 0 nedges
                         :width 1))
    (clkdel-assigns
         (vl-make-delay-assigns clkdelexprs clkexprs 1 atts))
    ((mv ddelexprs ddeldecls)
     (vl-occform-mkwires "ddel" 0 nedges
                         :width width))
    (ddel-assigns (vl-make-delay-assigns ddelexprs dexprs 1 atts))
    ((mv qdelexpr qdeldecl)
     (vl-occform-mkwire "qdel" width))
    (qdel-assigns
         (list (make-vl-assign :lvalue qdelexpr
                               :expr qregexpr
                               :delay (vl-make-constdelay 1)
                               :loc *vl-fakeloc*
                               :atts atts)))
    ((mv clkedgeexprs clkedgedecls)
     (vl-occform-mkwires "clkedge" 0 nedges
                         :width 1))
    (clkedge-assigns (vl-nedgeflop-clkedge-assigns
                          clkedgeexprs clkexprs clkdelexprs))
    (anyedge-rhs (vl-nedgeflop-or-edges clkedgeexprs))
    ((mv anyedgeexpr anyedgedecl)
     (vl-occform-mkwire "anyedge" 1))
    (anyedge-assign (make-vl-assign :lvalue anyedgeexpr
                                    :expr anyedge-rhs
                                    :loc *vl-fakeloc*))
    ((mv dfullexpr dfulldecl)
     (vl-occform-mkwire "dfull" width))
    (dfull-rhs (vl-nedgeflop-data-mux clkexprs ddelexprs width))
    (dfull-assign (make-vl-assign :lvalue dfullexpr
                                  :expr dfull-rhs
                                  :loc *vl-fakeloc*))
    (qassign
     (make-vl-assign
        :lvalue qregexpr
        :expr
        (make-vl-nonatom :op :vl-qmark
                         :args (list anyedgeexpr dfullexpr qdelexpr)
                         :finalwidth width
                         :finaltype :vl-unsigned
                         :atts (list (list "VL_LATCH_MUX")))
        :loc *vl-fakeloc*))
    (mod
     (make-vl-module
      :name name
      :origname name
      :ports (cons qport (append dports clkports))
      :portdecls (cons qportdecl
                       (append dportdecls clkportdecls))
      :vardecls
      (cons
       qvardecl
       (append
        dvardecls
        (append
         clkvardecls
         (append
          clkdeldecls
          (append
             ddeldecls
             (append
                  qregdecls
                  (cons qdeldecl
                        (append clkedgedecls
                                (cons anyedgedecl
                                      (cons dfulldecl 'nil))))))))))
      :assigns
      (append
       qregassigns
       (append
        clkdel-assigns
        (append
         ddel-assigns
         (append
            qdel-assigns
            (append
                 clkedge-assigns
                 (cons anyedge-assign
                       (cons dfull-assign (cons qassign 'nil))))))))
      :minloc *vl-fakeloc*
      :maxloc *vl-fakeloc*)))
   (list mod))))

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

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

Theorem: type-of-vl-make-nedgeflop-vec

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