Turn a VL assignment into an SVEX assignment or delayed assignment.
(vl-assign->svex-assign x ss scopes) → (mv vttree assigns)
This just straightforwardly converts the LHS and RHS to svex expressions, then converts the LHS into a sv::lhs-p.
At the moment we only support a single-tick delay, just because for a multi-tick we'd have to generate new names for the intermediate states.
Function:
(defun vl-assign->svex-assign (x ss scopes) (declare (xargs :guard (and (vl-assign-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (let ((__function__ 'vl-assign->svex-assign)) (declare (ignorable __function__)) (b* (((vl-assign x) (vl-assign-fix x)) (vttree nil) ((when (vl-expr-case x.lvalue :vl-stream)) (b* (((vmv vttree rhs ?rhs-type rhs-size) (vl-expr-to-svex-untyped x.expr ss scopes)) ((unless rhs-size) (mv vttree nil)) ((wvmv vttree delay :ctx x) (vl-maybe-gatedelay->delay x.delay)) (rhs (if delay (sv::svex-add-delay rhs delay) rhs)) ((vmv vttree assigns) (vl-streaming-unpack-to-svex-assign-top x.lvalue rhs x rhs-size ss scopes))) (mv vttree assigns))) ((vmv vttree lhs lhs-type :ctx x) (vl-expr-to-svex-lhs x.lvalue ss scopes)) ((unless lhs-type) (mv vttree nil)) ((wvmv vttree delay :ctx x) (vl-maybe-gatedelay->delay x.delay)) ((vmv vttree type-err svex-rhs :ctx x) (vl-expr-to-svex-datatyped x.expr x.lvalue lhs-type ss scopes :compattype :assign)) ((wvmv vttree :ctx x) (vl-type-error-basic-warn x.expr nil type-err x.lvalue lhs-type ss)) ((when (not delay)) (mv vttree (list (cons lhs (sv::make-driver :value svex-rhs))))) (svex-rhs (sv::svex-add-delay svex-rhs delay))) (mv vttree (list (cons lhs (sv::make-driver :value svex-rhs)))))))
Theorem:
(defthm return-type-of-vl-assign->svex-assign.vttree (b* (((mv ?vttree ?assigns) (vl-assign->svex-assign x ss scopes))) (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree))))) :rule-classes :rewrite)
Theorem:
(defthm assigns-p-of-vl-assign->svex-assign.assigns (b* (((mv ?vttree ?assigns) (vl-assign->svex-assign x ss scopes))) (sv::assigns-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-assign->svex-assign-assigns (b* (((mv ?vttree ?assigns) (vl-assign->svex-assign x ss scopes))) (sv::svarlist-addr-p (sv::assigns-vars assigns))))
Theorem:
(defthm vl-assign->svex-assign-of-vl-assign-fix-x (equal (vl-assign->svex-assign (vl-assign-fix x) ss scopes) (vl-assign->svex-assign x ss scopes)))
Theorem:
(defthm vl-assign->svex-assign-vl-assign-equiv-congruence-on-x (implies (vl-assign-equiv x x-equiv) (equal (vl-assign->svex-assign x ss scopes) (vl-assign->svex-assign x-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-assign->svex-assign-of-vl-scopestack-fix-ss (equal (vl-assign->svex-assign x (vl-scopestack-fix ss) scopes) (vl-assign->svex-assign x ss scopes)))
Theorem:
(defthm vl-assign->svex-assign-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-assign->svex-assign x ss scopes) (vl-assign->svex-assign x ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-assign->svex-assign-of-vl-elabscopes-fix-scopes (equal (vl-assign->svex-assign x ss (vl-elabscopes-fix scopes)) (vl-assign->svex-assign x ss scopes)))
Theorem:
(defthm vl-assign->svex-assign-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-assign->svex-assign x ss scopes) (vl-assign->svex-assign x ss scopes-equiv))) :rule-classes :congruence)