		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-1-bit-delay-m

Generate a one-bit wide, M-tick delay module.

Signature
(vl-make-1-bit-delay-m m) → 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 a module in terms of primitives that is equivalent to:

module VL_1_BIT_DELAY_M (out, in) ;
  output out;
  input in;
  assign #M out = in;
endmodule

When m is 1, this is just our primitive *vl-1-bit-delay-1* module.

When m is something larger than 1, we chain together m-many 1-tick delays to create an m-tick delay. For instance, a four-tick delay looks like this:

module VL_1_BIT_DELAY_4 (out, in) ;
  output out;
  input in;

  wire [2:0] temp;
  VL_1_BIT_DELAY_1 del1 (temp[0], in);
  VL_1_BIT_DELAY_1 del2 (temp[1], temp[0]);
  VL_1_BIT_DELAY_1 del3 (temp[2], temp[1]);
  VL_1_BIT_DELAY_1 del4 (out,     temp[2]);
endmodule

Definitions and Theorems

Function: vl-make-1-bit-delay-m

(defun vl-make-1-bit-delay-m (m)
 (declare (xargs :guard (posp m)))
 (let ((__function__ 'vl-make-1-bit-delay-m))
  (declare (ignorable __function__))
  (b*
   (((when (eql m 1))
     (list *vl-1-bit-delay-1*))
    (name (cat "VL_1_BIT_DELAY_" (natstr m)))
    ((mv out-expr
         out-port out-portdecl out-vardecl)
     (vl-occform-mkport "out" :vl-output 1))
    ((mv in-expr in-port in-portdecl in-vardecl)
     (vl-occform-mkport "in" :vl-input 1))
    ((mv temp-expr temp-vardecl)
     (vl-occform-mkwire "temp" (- m 1)))
    (temp-wires (vl-make-list-of-bitselects temp-expr 0 (- m 2)))
    (outs (append temp-wires (list out-expr)))
    (ins (cons in-expr temp-wires))
    (insts
     (vl-make-m-bit-delay-insts 1 "del"
                                (vl-module->name *vl-1-bit-delay-1*)
                                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 temp-vardecl)
              :modinsts insts
              :atts '(("VL_HANDS_OFF"))
              :minloc *vl-fakeloc*
              :maxloc *vl-fakeloc*)))
   (list mod *vl-1-bit-delay-1*))))

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

(defthm vl-modulelist-p-of-vl-make-1-bit-delay-m
  (b* ((mods (vl-make-1-bit-delay-m m)))
    (vl-modulelist-p mods))
  :rule-classes :rewrite)

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

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

Subtopics

Vl-make-m-bit-delay-insts