(vl-make-delay-assigns lhses rhses delay-amt atts) → assigns
Function:
(defun vl-make-delay-assigns (lhses rhses delay-amt atts) (declare (xargs :guard (and (vl-exprlist-p lhses) (vl-exprlist-p rhses) (natp delay-amt) (vl-atts-p atts)))) (declare (xargs :guard (equal (len lhses) (len rhses)))) (let ((__function__ 'vl-make-delay-assigns)) (declare (ignorable __function__)) (if (atom lhses) nil (cons (make-vl-assign :lvalue (car lhses) :expr (car rhses) :delay (vl-make-constdelay delay-amt) :atts atts :loc *vl-fakeloc*) (vl-make-delay-assigns (cdr lhses) (cdr rhses) delay-amt atts)))))
Theorem:
(defthm vl-assignlist-p-of-vl-make-delay-assigns (b* ((assigns (vl-make-delay-assigns lhses rhses delay-amt atts))) (vl-assignlist-p assigns)) :rule-classes :rewrite)