		Search-engine friendly clone of the ACL2 documentation.

Vl-make-n-bit-latch

Vl-make-1-bit-latch-instances

Build a list of VL_1_BIT_LATCH instances.

Signature
(vl-make-1-bit-latch-instances q-wires clk-wire d-wires &optional (n '0)) → insts
Arguments: q-wires — Guard (vl-exprlist-p q-wires).; clk-wire — Guard (vl-expr-p clk-wire).; d-wires — Guard (vl-exprlist-p d-wires).; n — current index, for name generation, counts up.
Guard (natp n).
Returns: insts — Type (vl-modinstlist-p insts).

We produce a list of latch instances like:

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_{n-1} (q[{n-1}], clk, d[{n-1}]) ;

Definitions and Theorems

Function: vl-make-1-bit-latch-instances-fn

(defun vl-make-1-bit-latch-instances-fn (q-wires clk-wire d-wires n)
  (declare (xargs :guard (and (vl-exprlist-p q-wires)
                              (vl-expr-p clk-wire)
                              (vl-exprlist-p d-wires)
                              (natp n))))
  (declare (xargs :guard (same-lengthp q-wires d-wires)))
  (let ((__function__ 'vl-make-1-bit-latch-instances))
    (declare (ignorable __function__))
    (if (atom q-wires)
        nil
      (cons (vl-simple-inst *vl-1-bit-latch*
                            (hons-copy (cat "bit_" (natstr n)))
                            (car q-wires)
                            clk-wire (car d-wires))
            (vl-make-1-bit-latch-instances (cdr q-wires)
                                           clk-wire (cdr d-wires)
                                           (+ n 1))))))

Theorem: vl-modinstlist-p-of-vl-make-1-bit-latch-instances

(defthm vl-modinstlist-p-of-vl-make-1-bit-latch-instances
 (b*
  ((insts
     (vl-make-1-bit-latch-instances-fn q-wires clk-wire d-wires n)))
  (vl-modinstlist-p insts))
 :rule-classes :rewrite)