(vl-make-m-bit-delay-insts n basename modname outs ins) → modinsts
Function:
(defun vl-make-m-bit-delay-insts (n basename modname outs ins) (declare (xargs :guard (and (natp n) (stringp basename) (stringp modname) (vl-exprlist-p outs) (vl-exprlist-p ins)))) (declare (xargs :guard (same-lengthp outs ins))) (let ((__function__ 'vl-make-m-bit-delay-insts)) (declare (ignorable __function__)) (b* (((when (atom outs)) nil) (args (list (make-vl-plainarg :expr (car outs) :dir :vl-output :portname "out") (make-vl-plainarg :expr (car ins) :dir :vl-input :portname "in")))) (cons (make-vl-modinst :instname (cat basename (natstr n)) :modname modname :paramargs (make-vl-paramargs-plain :args nil) :portargs (make-vl-arguments-plain :args args) :loc *vl-fakeloc*) (vl-make-m-bit-delay-insts (+ n 1) basename modname (cdr outs) (cdr ins))))))
Theorem:
(defthm vl-modinstlist-p-of-vl-make-m-bit-delay-insts (implies (and (force (natp n)) (force (stringp basename)) (force (stringp modname)) (force (vl-exprlist-p outs)) (force (vl-exprlist-p ins)) (force (same-lengthp outs ins))) (b* ((modinsts (vl-make-m-bit-delay-insts n basename modname outs ins))) (vl-modinstlist-p modinsts))) :rule-classes :rewrite)