Checks that the always block is suitable for translating to svex, ~ and returns the body statement and eventcontrol.
(vl-always->svex-checks x ss scopes) → (mv ok warnings stmt trigger trigger-subst)
Function:
(defun vl-always->svex-checks (x ss scopes) (declare (xargs :guard (and (vl-always-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (let ((__function__ 'vl-always->svex-checks)) (declare (ignorable __function__)) (b* (((vl-always x) (vl-always-fix x)) (warnings nil)) (case x.type ((:vl-always-comb :vl-always-latch) (mv t (ok) x.stmt nil nil)) (otherwise (b* (((unless (and (eq (vl-stmt-kind x.stmt) :vl-timingstmt) (eq (tag (vl-timingstmt->ctrl x.stmt)) :vl-eventcontrol))) (mv nil (warn :type :vl-always->svex-fail :msg "We only support always and always_ff blocks ~ that have a sensitivity list." :args (list x)) nil nil nil)) ((vl-timingstmt x.stmt)) ((when (or (vl-eventcontrol->starp x.stmt.ctrl) (not (vl-evatomlist-has-edge (vl-eventcontrol->atoms x.stmt.ctrl))))) (b* ((warnings (if (eq x.type :vl-always-ff) (warn :type :vl-always-ff-warning :msg "Always_ff is not edge-triggered." :args (list x)) (ok)))) (mv t (ok) x.stmt.body nil nil))) ((wmv warnings trigger) (vl-evatomlist->svex (vl-eventcontrol->atoms x.stmt.ctrl) ss scopes)) ((wmv warnings trigger-subst) (vl-evatomlist-delay-substitution (vl-eventcontrol->atoms x.stmt.ctrl) t ss scopes))) (mv t warnings x.stmt.body trigger trigger-subst)))))))
Theorem:
(defthm vl-warninglist-p-of-vl-always->svex-checks.warnings (b* (((mv ?ok ?warnings ?stmt ?trigger ?trigger-subst) (vl-always->svex-checks x ss scopes))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-always->svex-checks.stmt (b* (((mv ?ok ?warnings ?stmt ?trigger ?trigger-subst) (vl-always->svex-checks x ss scopes))) (implies ok (vl-stmt-p stmt))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-always->svex-checks.trigger (b* (((mv ?ok ?warnings ?stmt ?trigger ?trigger-subst) (vl-always->svex-checks x ss scopes))) (and (iff (sv::svex-p trigger) trigger) (implies trigger (sv::svarlist-addr-p (sv::svex-vars trigger))))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-always->svex-checks.trigger-subst (b* (((mv ?ok ?warnings ?stmt ?trigger ?trigger-subst) (vl-always->svex-checks x ss scopes))) (and (sv::svex-alist-p trigger-subst) (sv::svarlist-addr-p (sv::svex-alist-vars trigger-subst)) (sv::svarlist-addr-p (sv::svex-alist-keys trigger-subst)))) :rule-classes :rewrite)
Theorem:
(defthm vl-always->svex-checks-of-vl-always-fix-x (equal (vl-always->svex-checks (vl-always-fix x) ss scopes) (vl-always->svex-checks x ss scopes)))
Theorem:
(defthm vl-always->svex-checks-vl-always-equiv-congruence-on-x (implies (vl-always-equiv x x-equiv) (equal (vl-always->svex-checks x ss scopes) (vl-always->svex-checks x-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-always->svex-checks-of-vl-scopestack-fix-ss (equal (vl-always->svex-checks x (vl-scopestack-fix ss) scopes) (vl-always->svex-checks x ss scopes)))
Theorem:
(defthm vl-always->svex-checks-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-always->svex-checks x ss scopes) (vl-always->svex-checks x ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-always->svex-checks-of-vl-elabscopes-fix-scopes (equal (vl-always->svex-checks x ss (vl-elabscopes-fix scopes)) (vl-always->svex-checks x ss scopes)))
Theorem:
(defthm vl-always->svex-checks-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-always->svex-checks x ss scopes) (vl-always->svex-checks x ss scopes-equiv))) :rule-classes :congruence)