(vl-cblock-make-assign name vars body ctx) → assigns
Function:
(defun vl-cblock-make-assign (name vars body ctx) (declare (xargs :guard (and (stringp name) (vl-vardecllist-p vars) (vl-stmt-p body) (vl-always-p ctx)))) (declare (xargs :guard (vl-stmt-cblock-p body))) (let ((__function__ 'vl-cblock-make-assign)) (declare (ignorable __function__)) (b* ((decl (vl-find-vardecl name vars)) ((unless decl) (raise "Failed to find reg decl for ~x0??" name)) ((unless (and (vl-simplereg-p decl) (vl-maybe-range-resolved-p (vl-simplereg->range decl)))) (raise "Variable decl too hard for ~x0??" name)) (size (vl-maybe-range-size (vl-simplereg->range decl))) (type (if (vl-simplereg->signedp decl) :vl-signed :vl-unsigned)) (initial-x (make-vl-atom :guts (make-vl-weirdint :origwidth size :origtype :vl-unsigned :bits (repeat size :vl-xval) :wasunsized nil) :finalwidth size :finaltype :vl-unsigned)) (expr (vl-stmt-cblock-varexpr name body initial-x)) (lhs (vl-idexpr name size type)) (assign (make-vl-assign :lvalue lhs :expr expr :atts (acons "VL_COMBINATIONAL_BLOCK" nil nil) :loc (vl-always->loc ctx)))) (list assign))))
Theorem:
(defthm vl-assignlist-p-of-vl-cblock-make-assign (implies (and (force (stringp name)) (force (vl-vardecllist-p vars)) (force (vl-stmt-p body)) (force (vl-always-p ctx)) (force (vl-stmt-cblock-p body))) (b* ((assigns (vl-cblock-make-assign name vars body ctx))) (vl-assignlist-p assigns))) :rule-classes :rewrite)