Translate a combinational or latch-type always block into a set of SVEX expressions.
(vl-always->svex x ss scopes config) → (mv warnings assigns constraints)
Function:
(defun vl-always->svex (x ss scopes config) (declare (xargs :guard (and (vl-always-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes) (vl-simpconfig-p config)))) (let ((__function__ 'vl-always->svex)) (declare (ignorable __function__)) (b* ((warnings nil) ((vl-simpconfig config)) ((vl-always x) (vl-always-fix x)) ((wmv ok warnings stmt trigger trigger-subst :ctx x) (vl-always->svex-checks x ss scopes)) ((unless ok) (mv warnings nil nil)) ((wmv ok warnings svstmts :ctx x) (vl-stmt->svstmts stmt ss scopes (make-svstmt-config :nonblockingp t :uniquecase-conservative config.uniquecase-conservative :uniquecase-constraints config.uniquecase-constraints) nil)) ((unless ok) (mv warnings nil nil)) (locstring (vl-location-string x.loc)) ((wmv ok warnings st constraints blkst-write-masks nbst-write-masks :ctx x) (time$ (sv::svstmtlist-compile-top svstmts :sclimit config.sc-limit :nb-delayp nil) :mintime 1/2 :msg "; vl-always->svex: compiling statement at ~s0: ~st sec, ~sa bytes~%" :args (list locstring))) ((unless ok) (mv warnings nil nil)) ((sv::svstate st) (sv::svstate-clean st)) (- (sv::svstack-free st.blkst)) (st.blkst (make-fast-alist (sv::svstack-to-svex-alist st.blkst))) (st.nonblkst (sv::svex-alist-unset-nonblocking st.nonblkst)) (blk-written-vars (sv::svex-alist-keys st.blkst)) (nb-written-vars (sv::svex-alist-keys st.nonblkst)) (both-written (acl2::hons-intersection blk-written-vars nb-written-vars)) ((when both-written) (mv (warn :type :vl-always->svex-fail :msg "~a0: Variables written by both blocking and ~ nonblocking assignments: ~x1" :args (list x both-written)) nil nil)) (written-vars (append blk-written-vars nb-written-vars)) (nb-read-vars (sv::svex-alist-vars st.nonblkst)) (loc-of-interest nil) (- (and loc-of-interest (sneaky-save 'blkst st.blkst)) (and loc-of-interest (sneaky-save 'nonblkst st.nonblkst))) (blkst-rw (time$ (sv::svex-alist-maybe-rewrite-fixpoint st.blkst config.sv-simplify :verbosep config.sv-simplify-verbosep) :mintime (if loc-of-interest 0 1/2) :msg "; vl-always->svex at ~s0: rewriting blocking assignments: ~st sec, ~sa bytes~%" :args (list locstring))) (nbst-rw (time$ (sv::svex-alist-maybe-rewrite-fixpoint st.nonblkst config.sv-simplify :verbosep config.sv-simplify-verbosep) :mintime (if loc-of-interest 0 1/2) :msg "; vl-always->svex at ~s0: rewriting nonblocking assignments: ~st sec, ~sa bytes~%" :args (list locstring))) (constraints-rw (time$ (sv::constraintlist-maybe-rewrite-fixpoint constraints config.sv-simplify :verbosep config.sv-simplify-verbosep) :mintime (if loc-of-interest 0 1/2) :msg "; vl-always->svex at ~s0: rewriting constraints: ~st sec, ~sa bytes~%" :args (list locstring))) (read-masks (time$ (sv::svexlist-mask-alist (append (sv::svex-alist-vals blkst-rw) (sv::svex-alist-vals nbst-rw))) :mintime (if loc-of-interest 0 1/2) :msg "; vl-always->svex at ~s0: read masks: ~st sec, ~sa bytes~%" :args (list locstring))) (nbst-write-masks (make-fast-alist (sv::4vmask-alist-unset-nonblocking (fast-alist-free nbst-write-masks)))) (- (clear-memoize-table 'sv::svex-unset-nonblocking) (clear-memoize-table 'sv::svex-set-nonblocking)) (write-masks (fast-alist-clean (combine-mask-alists blkst-write-masks nbst-write-masks))) (subst (if (eq x.type :vl-always-comb) (sv::svarlist-masked-x-subst written-vars write-masks) (sv::svarlist-delay-subst written-vars))) ((wmv warnings :ctx x) (if (eq x.type :vl-always-comb) (vl-always->svex-latch-warnings write-masks read-masks) warnings)) ((with-fast subst)) (blkst-subst (sv::svex-alist-compose blkst-rw subst)) (nbst-subst (sv::svex-alist-compose nbst-rw subst)) (constraints-subst (sv::constraintlist-compose constraints-rw subst)) (nbst-trigger (if trigger (b* ((nb-delaysubst (append-without-guard trigger-subst (sv::svarlist-delay-subst nb-read-vars))) (nbst-subst2 (with-fast-alist nb-delaysubst (sv::svex-alist-compose nbst-subst nb-delaysubst)))) (vl-always-apply-trigger-to-updates trigger nbst-subst2)) (if config.nb-latch-delay-hack (sv::svex-alist-add-delay nbst-subst 1) nbst-subst))) (blkst-trigger (if trigger (vl-always-apply-trigger-to-updates trigger blkst-subst) blkst-subst)) (constraints-trigger (if trigger (sv::constraintlist-add-pathcond trigger nil constraints-subst) constraints-subst)) (updates (append nbst-trigger blkst-trigger)) (- (and loc-of-interest (sneaky-save 'updates updates))) (- (and loc-of-interest (break$))) (updates-rw (time$ (sv::svex-alist-maybe-rewrite-fixpoint updates config.sv-simplify :verbosep config.sv-simplify-verbosep) :mintime (if loc-of-interest 0 1/2) :msg "; vl-always->svex at ~s0: rewriting final updates: ~st sec, ~sa bytes~%" :args (list (vl-location-string x.loc)))) (lhs-sizes (make-fast-alist (sv::svstmtlist-lhs-var-sizes svstmts (list nil) nil))) (assigns (sv::svex-alist->assigns updates-rw lhs-sizes write-masks))) (mv warnings assigns constraints-trigger))))
Theorem:
(defthm vl-warninglist-p-of-vl-always->svex.warnings (b* (((mv ?warnings ?assigns ?constraints) (vl-always->svex x ss scopes config))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-always->svex.assigns (b* (((mv ?warnings ?assigns ?constraints) (vl-always->svex x ss scopes config))) (and (sv::assigns-p assigns) (sv::svarlist-addr-p (sv::assigns-vars assigns)))) :rule-classes :rewrite)
Theorem:
(defthm constraintlist-p-of-vl-always->svex.constraints (b* (((mv ?warnings ?assigns ?constraints) (vl-always->svex x ss scopes config))) (sv::constraintlist-p constraints)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-always->svex (b* (((mv ?warnings ?assigns ?constraints) (vl-always->svex x ss scopes config))) (and (sv::svarlist-addr-p (sv::assigns-vars assigns)) (sv::svarlist-addr-p (sv::constraintlist-vars constraints)))))
Theorem:
(defthm vl-always->svex-of-vl-always-fix-x (equal (vl-always->svex (vl-always-fix x) ss scopes config) (vl-always->svex x ss scopes config)))
Theorem:
(defthm vl-always->svex-vl-always-equiv-congruence-on-x (implies (vl-always-equiv x x-equiv) (equal (vl-always->svex x ss scopes config) (vl-always->svex x-equiv ss scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-always->svex-of-vl-scopestack-fix-ss (equal (vl-always->svex x (vl-scopestack-fix ss) scopes config) (vl-always->svex x ss scopes config)))
Theorem:
(defthm vl-always->svex-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-always->svex x ss scopes config) (vl-always->svex x ss-equiv scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-always->svex-of-vl-elabscopes-fix-scopes (equal (vl-always->svex x ss (vl-elabscopes-fix scopes) config) (vl-always->svex x ss scopes config)))
Theorem:
(defthm vl-always->svex-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-always->svex x ss scopes config) (vl-always->svex x ss scopes-equiv config))) :rule-classes :congruence)
Theorem:
(defthm vl-always->svex-of-vl-simpconfig-fix-config (equal (vl-always->svex x ss scopes (vl-simpconfig-fix config)) (vl-always->svex x ss scopes config)))
Theorem:
(defthm vl-always->svex-vl-simpconfig-equiv-congruence-on-config (implies (vl-simpconfig-equiv config config-equiv) (equal (vl-always->svex x ss scopes config) (vl-always->svex x ss scopes config-equiv))) :rule-classes :congruence)