Update our current expression for
(vl-atomicstmt-cblock-varexpr varname x curr) → expr?
Function:
(defun vl-atomicstmt-cblock-varexpr (varname x curr) (declare (xargs :guard (and (stringp varname) (and (vl-stmt-p x) (vl-atomicstmt-p x)) (vl-expr-p curr)))) (declare (xargs :guard (vl-atomicstmt-cblock-p x))) (let ((__function__ 'vl-atomicstmt-cblock-varexpr)) (declare (ignorable __function__)) (case (vl-stmt-kind x) (:vl-nullstmt curr) (:vl-assignstmt (b* (((unless (equal varname (vl-idexpr->name (vl-assignstmt->lvalue x)))) curr) (expr (vl-assignstmt->expr x)) (finalwidth (vl-expr->finalwidth expr)) (- (or (posp finalwidth) (raise "No size on expression."))) (wrapper (make-vl-nonatom :op :vl-concat :args (list expr) :finalwidth finalwidth :finaltype :vl-unsigned))) wrapper)) (otherwise curr))))
Theorem:
(defthm vl-expr-p-of-vl-atomicstmt-cblock-varexpr (implies (and (force (stringp varname)) (force (if (vl-stmt-p x) (vl-atomicstmt-p x) 'nil)) (force (vl-expr-p curr)) (force (vl-atomicstmt-cblock-p x))) (b* ((expr? (vl-atomicstmt-cblock-varexpr varname x curr))) (vl-expr-p expr?))) :rule-classes :rewrite)