		Search-engine friendly clone of the ACL2 documentation.

Latchcode

Vl-make-n-bit-latch

Generate an N-bit latch module.

Signature
(vl-make-n-bit-latch n) → 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 that is written in terms of primitives and is semantically equivalent to:

module VL_N_BIT_LATCH (q, clk, d);
  output q;
  input clk;
  input d;
  reg q;
  always @(d or clk)
    q <= clk ? d : q;
endmodule

The actual definition uses a list of *vl-1-bit-latch* primitives, e.g., for the four-bit case we would have:

module VL_4_BIT_LATCH (q, clk, d);
  output [3:0] q;
  input clk;
  input [3:0] d;

  VL_1_BIT_LATCH bit_0 (q[0], clk, d[0]);
  VL_1_BIT_LATCH bit_1 (q[1], clk, d[1]);
  VL_1_BIT_LATCH bit_2 (q[2], clk, d[2]);
  VL_1_BIT_LATCH bit_3 (q[3], clk, d[3]);
endmodule

Definitions and Theorems

Function: vl-make-n-bit-latch

(defun vl-make-n-bit-latch (n)
 (declare (xargs :guard (posp n)))
 (let ((__function__ 'vl-make-n-bit-latch))
  (declare (ignorable __function__))
  (b*
   (((when (eql n 1))
     (list *vl-1-bit-latch*))
    (name (hons-copy (cat "VL_" (natstr n) "_BIT_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))
    (q-wires (vl-make-list-of-bitselects q-expr 0 (- n 1)))
    (d-wires (vl-make-list-of-bitselects d-expr 0 (- n 1)))
    (modinsts
        (vl-make-1-bit-latch-instances q-wires clk-expr d-wires 0)))
   (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)
              :modinsts modinsts
              :atts (acons "VL_HANDS_OFF" nil nil)
              :minloc *vl-fakeloc*
              :maxloc *vl-fakeloc*)
         *vl-1-bit-latch*))))

Theorem: vl-modulelist-p-of-vl-make-n-bit-latch

(defthm vl-modulelist-p-of-vl-make-n-bit-latch
  (b* ((mods (vl-make-n-bit-latch n)))
    (vl-modulelist-p mods))
  :rule-classes :rewrite)

Theorem: type-of-vl-make-n-bit-latch

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

Subtopics

Vl-make-1-bit-latch-instances: Build a list of VL_1_BIT_LATCH instances.