		Search-engine friendly clone of the ACL2 documentation.

Latchcode

Vl-make-n-bit-latch-vec

Generate an N-bit latch module for vector-oriented synthesis.

Signature
(vl-make-n-bit-latch-vec n del) → 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).

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

Definitions and Theorems

Function: vl-make-n-bit-latch-vec

(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: vl-modulelist-p-of-vl-make-n-bit-latch-vec

(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: type-of-vl-make-n-bit-latch-vec

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