Build a list of
(vl-make-1-bit-latch-instances q-wires clk-wire d-wires &optional (n '0)) → 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}]) ;
Function:
(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:
(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)