(vl-evatomlist->svex x ss scopes) → (mv warnings trigger)
Function:
(defun vl-evatomlist->svex (x ss scopes) (declare (xargs :guard (and (vl-evatomlist-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (let ((__function__ 'vl-evatomlist->svex)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil (sv::svex-quote (sv::2vec 0)))) ((vl-evatom x1) (car x)) (warnings nil) ((vwmv vttree expr ?type ?size) (vl-expr-to-svex-untyped x1.expr ss scopes)) (delay-expr (sv::svex-add-delay expr 1)) (trigger1 (case x1.type (:vl-noedge (sv::svcall sv::bitnot (sv::svcall sv::== expr delay-expr))) (:vl-posedge (sv::svcall sv::uor (sv::svcall sv::bitand (sv::svcall sv::bitnot (sv::svex-zerox 1 delay-expr)) (sv::svex-zerox 1 expr)))) (:vl-negedge (sv::svcall sv::uor (sv::svcall sv::bitand (sv::svcall sv::bitnot (sv::svex-zerox 1 expr)) (sv::svex-zerox 1 delay-expr)))) (:vl-edge (sv::svcall sv::uor (sv::svcall sv::bitxor (sv::svex-zerox 1 expr) (sv::svex-zerox 1 delay-expr)))))) ((wmv warnings rest) (vl-evatomlist->svex (cdr x) ss scopes))) (mv warnings (sv::make-svex-call :fn 'sv::bitor :args (list trigger1 rest))))))
Theorem:
(defthm vl-warninglist-p-of-vl-evatomlist->svex.warnings (b* (((mv ?warnings ?trigger) (vl-evatomlist->svex x ss scopes))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-evatomlist->svex.trigger (b* (((mv ?warnings ?trigger) (vl-evatomlist->svex x ss scopes))) (and (sv::svex-p trigger) (sv::svarlist-addr-p (sv::svex-vars trigger)))) :rule-classes :rewrite)
Theorem:
(defthm vl-evatomlist->svex-of-vl-evatomlist-fix-x (equal (vl-evatomlist->svex (vl-evatomlist-fix x) ss scopes) (vl-evatomlist->svex x ss scopes)))
Theorem:
(defthm vl-evatomlist->svex-vl-evatomlist-equiv-congruence-on-x (implies (vl-evatomlist-equiv x x-equiv) (equal (vl-evatomlist->svex x ss scopes) (vl-evatomlist->svex x-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-evatomlist->svex-of-vl-scopestack-fix-ss (equal (vl-evatomlist->svex x (vl-scopestack-fix ss) scopes) (vl-evatomlist->svex x ss scopes)))
Theorem:
(defthm vl-evatomlist->svex-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-evatomlist->svex x ss scopes) (vl-evatomlist->svex x ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-evatomlist->svex-of-vl-elabscopes-fix-scopes (equal (vl-evatomlist->svex x ss (vl-elabscopes-fix scopes)) (vl-evatomlist->svex x ss scopes)))
Theorem:
(defthm vl-evatomlist->svex-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-evatomlist->svex x ss scopes) (vl-evatomlist->svex x ss scopes-equiv))) :rule-classes :congruence)