		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-delay-m

Generate an N-bit wide, M-tick delay module.

Signature
(vl-make-n-bit-delay-m n m &key vecp) → mods
Arguments: n — Guard (posp n).; m — Guard (posp m).
Returns: mods — Type (vl-modulelist-p mods), given the guard.

We generate a module in terms of primitives that is equivalent to:

module VL_N_BIT_DELAY_M (out, in) ;
  output [N-1:0] out;
  input [N-1:0] in;
  assign #M out = in;
endmodule

In the special case that m is 1, we build a VL_N_BIT_DELAY_1 module using vl-make-n-bit-delay-1.

Otherwise, we just chain together a list of these modules, one for each tick. For instance, a module that implements 4-bit wide delay for 3 ticks would look like this:

module VL_4_BIT_DELAY_3 (out, in);
  output [3:0] out;
  output [3:0] in;

  wire [3:0] temp1;
  wire [3:0] temp2;

  VL_4_BIT_DELAY_1 bit0 (temp1, in);
  VL_4_BIT_DELAY_1 bit1 (temp2, temp1);
  VL_4_BIT_DELAY_1 bit2 (out, temp2);
endmodule

Definitions and Theorems

Function: vl-make-n-bit-delay-m-fn

(defun vl-make-n-bit-delay-m-fn (n m vecp)
 (declare (xargs :guard (and (posp n) (posp m))))
 (let ((__function__ 'vl-make-n-bit-delay-m))
   (declare (ignorable __function__))
   (b*
    ((base (vl-make-n-bit-delay-1 n :vecp vecp))
     ((when (= m 1)) base)
     (name (cat "VL_" (natstr n)
                "_BIT_DELAY_" (natstr m)))
     ((mv out-expr
          out-port out-portdecl out-vardecl)
      (vl-occform-mkport "out" :vl-output n))
     ((mv in-expr in-port in-portdecl in-vardecl)
      (vl-occform-mkport "in" :vl-input n))
     ((mv tmp-exprs tmp-vardecls)
      (vl-occform-mkwires "temp" 1 m
                          :width n))
     (outs (append tmp-exprs (list out-expr)))
     (ins (cons in-expr tmp-exprs))
     (insts (vl-simple-inst-list (car base)
                                 "del" outs ins))
     (mod (make-vl-module
               :name name
               :origname name
               :ports (list out-port in-port)
               :portdecls (list out-portdecl in-portdecl)
               :vardecls (list* out-vardecl in-vardecl tmp-vardecls)
               :modinsts insts
               :minloc *vl-fakeloc*
               :maxloc *vl-fakeloc*)))
    (cons mod base))))

Theorem: vl-modulelist-p-of-vl-make-n-bit-delay-m

(defthm vl-modulelist-p-of-vl-make-n-bit-delay-m
  (implies (and (posp n) (posp m))
           (b* ((mods (vl-make-n-bit-delay-m-fn n m vecp)))
             (vl-modulelist-p mods)))
  :rule-classes :rewrite)

Theorem: type-of-vl-make-n-bit-delay-m

(defthm type-of-vl-make-n-bit-delay-m
  (and (true-listp (vl-make-n-bit-delay-m n m :vecp vecp))
       (consp (vl-make-n-bit-delay-m n m :vecp vecp)))
  :rule-classes :type-prescription)