Generate assignments that supply the inputs to a function call.
(vl-fun-make-assignments-to-inputs netnames actuals loc) → assigns
Function:
(defun vl-fun-make-assignments-to-inputs (netnames actuals loc) (declare (xargs :guard (and (string-listp netnames) (vl-exprlist-p actuals) (vl-location-p loc)))) (declare (xargs :guard (same-lengthp netnames actuals))) (let ((__function__ 'vl-fun-make-assignments-to-inputs)) (declare (ignorable __function__)) (if (atom netnames) nil (cons (make-vl-assign :lvalue (vl-idexpr (car netnames) nil nil) :expr (car actuals) :loc loc) (vl-fun-make-assignments-to-inputs (cdr netnames) (cdr actuals) loc)))))
Theorem:
(defthm vl-assignlist-p-of-vl-fun-make-assignments-to-inputs (b* ((assigns (vl-fun-make-assignments-to-inputs netnames actuals loc))) (vl-assignlist-p assigns)) :rule-classes :rewrite)