Safely merge
(vl-edgesynth-merge-data-ifs condition true-branch false-branch nf vardecls assigns) → (mv new-stmt nf vardecls assigns)
Assumption: any assignments are to the same register.
Function:
(defun vl-edgesynth-merge-data-ifs (condition true-branch false-branch nf vardecls assigns) (declare (xargs :guard (and (vl-expr-p condition) (and (vl-stmt-p true-branch) (vl-atomicstmt-p true-branch) (vl-edgesynth-stmt-p true-branch)) (and (vl-stmt-p false-branch) (vl-atomicstmt-p false-branch) (vl-edgesynth-stmt-p false-branch)) (vl-namefactory-p nf) (vl-vardecllist-p vardecls) (vl-assignlist-p assigns)))) (let ((__function__ 'vl-edgesynth-merge-data-ifs)) (declare (ignorable __function__)) (b* (((when (and (vl-nullstmt-p true-branch) (vl-nullstmt-p false-branch))) (mv true-branch nf vardecls assigns)) (base-assign (if (vl-assignstmt-p true-branch) true-branch false-branch)) (target-reg (vl-assignstmt->lvalue base-assign)) (loc (vl-assignstmt->loc base-assign)) (width (vl-expr->finalwidth target-reg)) (true-rhs (if (vl-assignstmt-p true-branch) (vl-assignstmt->expr true-branch) target-reg)) (false-rhs (if (vl-assignstmt-p false-branch) (vl-assignstmt->expr false-branch) target-reg)) (basename (cat (vl-idexpr->name target-reg) "_next")) ((mv true-name nf) (vl-namefactory-indexed-name basename nf)) ((mv false-name nf) (vl-namefactory-indexed-name basename nf)) ((mv true-expr true-decl) (vl-occform-mkwire true-name width :loc loc)) ((mv false-expr false-decl) (vl-occform-mkwire false-name width :loc loc)) (true-assign (make-vl-assign :lvalue true-expr :expr true-rhs :loc loc)) (false-assign (make-vl-assign :lvalue false-expr :expr false-rhs :loc loc)) (vardecls (list* true-decl false-decl vardecls)) (assigns (list* true-assign false-assign assigns)) (new-rhs (vl-safe-qmark-expr condition true-expr false-expr)) (new-stmt (change-vl-assignstmt base-assign :expr new-rhs))) (mv new-stmt nf vardecls assigns))))
Theorem:
(defthm vl-edgesynth-stmt-p-of-vl-edgesynth-merge-data-ifs.new-stmt (implies (and (force (vl-expr-p condition)) (force (vl-edgesynth-stmt-p true-branch)) (force (vl-edgesynth-stmt-p false-branch)) (force (vl-atomicstmt-p true-branch)) (force (vl-atomicstmt-p false-branch))) (b* (((mv ?new-stmt ?nf ?vardecls ?assigns) (vl-edgesynth-merge-data-ifs condition true-branch false-branch nf vardecls assigns))) (vl-edgesynth-stmt-p new-stmt))) :rule-classes :rewrite)
Theorem:
(defthm vl-namefactory-p-of-vl-edgesynth-merge-data-ifs.nf (implies (force (vl-namefactory-p nf)) (b* (((mv ?new-stmt ?nf ?vardecls ?assigns) (vl-edgesynth-merge-data-ifs condition true-branch false-branch nf vardecls assigns))) (vl-namefactory-p nf))) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecllist-p-of-vl-edgesynth-merge-data-ifs.vardecls (implies (and (force (vl-expr-p condition)) (force (if (vl-stmt-p true-branch) (if (vl-atomicstmt-p true-branch) (vl-edgesynth-stmt-p true-branch) 'nil) 'nil)) (force (if (vl-stmt-p false-branch) (if (vl-atomicstmt-p false-branch) (vl-edgesynth-stmt-p false-branch) 'nil) 'nil)) (force (vl-namefactory-p nf)) (force (vl-vardecllist-p vardecls)) (force (vl-assignlist-p assigns))) (b* (((mv ?new-stmt ?nf ?vardecls ?assigns) (vl-edgesynth-merge-data-ifs condition true-branch false-branch nf vardecls assigns))) (vl-vardecllist-p vardecls))) :rule-classes :rewrite)
Theorem:
(defthm vl-assignlist-p-of-vl-edgesynth-merge-data-ifs.assigns (implies (and (force (vl-expr-p condition)) (force (if (vl-stmt-p true-branch) (if (vl-atomicstmt-p true-branch) (vl-edgesynth-stmt-p true-branch) 'nil) 'nil)) (force (if (vl-stmt-p false-branch) (if (vl-atomicstmt-p false-branch) (vl-edgesynth-stmt-p false-branch) 'nil) 'nil)) (force (vl-namefactory-p nf)) (force (vl-vardecllist-p vardecls)) (force (vl-assignlist-p assigns))) (b* (((mv ?new-stmt ?nf ?vardecls ?assigns) (vl-edgesynth-merge-data-ifs condition true-branch false-branch nf vardecls assigns))) (vl-assignlist-p assigns))) :rule-classes :rewrite)