		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-delay-1

Generate an n-bit wide, 1-tick delay module.

Signature
(vl-make-n-bit-delay-1 n &key vecp) → mods
Arguments: n — Guard (posp n).
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), given the guard.

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

module VL_n_BIT_DELAY_1 (out, in) ;
  output [n-1:0] out;
  input [n-1:0] in;
  assign #1 out = in;
endmodule

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

When n is something larger than 1, then if vecp is true we just make the module above. Otherwise, we instantiate n 1-bit delays. For instance, a four-bit delay looks like this:

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

  VL_1_BIT_DELAY_1 del0 (out[0], in[0]);
  VL_1_BIT_DELAY_1 del1 (out[1], in[1]);
  VL_1_BIT_DELAY_1 del2 (out[2], in[2]);
  VL_1_BIT_DELAY_1 del3 (out[3], in[3]);
endmodule

Definitions and Theorems

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

(defun vl-make-n-bit-delay-1-fn (n vecp)
 (declare (xargs :guard (posp n)))
 (let ((__function__ 'vl-make-n-bit-delay-1))
  (declare (ignorable __function__))
  (b*
   (((when (eql n 1))
     (list *vl-1-bit-delay-1*))
    (name (cat "VL_" (natstr n) "_BIT_DELAY_1"))
    ((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))
    ((when vecp)
     (b*
      ((assign
            (make-vl-assign
                 :lvalue out-expr
                 :expr in-expr
                 :delay (make-vl-gatedelay :rise (vl-make-index 1)
                                           :fall (vl-make-index 1))
                 :loc *vl-fakeloc*))
       (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)
         :assigns (list assign)
         :minloc *vl-fakeloc*
         :atts (cons (cons '"VL_SVEX_PRIMITIVE"
                           (make-vl-atom :guts (vl-string "delay")))
                     (cons (cons '"VL_SVEX_PRIMITIVE_WIDTH"
                                 (vl-make-index n))
                           '(("VL_HANDS_OFF"))))
         :maxloc *vl-fakeloc*)))
      (list mod)))
    (outs (vl-make-list-of-bitselects out-expr 0 (1- n)))
    (ins (vl-make-list-of-bitselects in-expr 0 (1- n)))
    (insts (vl-simple-inst-list *vl-1-bit-delay-1* "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)
                         :modinsts insts
                         :minloc *vl-fakeloc*
                         :maxloc *vl-fakeloc*)))
   (list mod *vl-1-bit-delay-1*))))

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

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

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

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