Recognize and decompose edge-triggered statements.
(vl-match-always-at-some-edges x) → (mv body? ctrl? edges)
Function:
(defun vl-match-always-at-some-edges (x) (declare (xargs :guard (vl-stmt-p x))) (let ((__function__ 'vl-match-always-at-some-edges)) (declare (ignorable __function__)) (b* (((unless (eq (vl-stmt-kind x) :vl-timingstmt)) (mv nil nil nil)) ((vl-timingstmt x) x) ((unless (vl-edge-control-p x.ctrl)) (mv nil nil nil))) (mv x.body x.ctrl (vl-eventcontrol->atoms x.ctrl)))))
Theorem:
(defthm return-type-of-vl-match-always-at-some-edges.body? (b* (((mv ?body? ?ctrl? ?edges) (vl-match-always-at-some-edges x))) (equal (vl-stmt-p body?) (if body? t nil))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-match-always-at-some-edges.ctrl? (b* (((mv ?body? ?ctrl? ?edges) (vl-match-always-at-some-edges x))) (and (equal (vl-eventcontrol-p ctrl?) (if body? t nil)) (equal (vl-edge-control-p ctrl?) (if body? t nil)))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-match-always-at-some-edges.edges (b* (((mv ?body? ?ctrl? ?edges) (vl-match-always-at-some-edges x))) (and (vl-evatomlist-p edges) (vl-evatomlist-all-have-edges-p edges) (equal (consp edges) (if body? t nil)) (iff edges body?))) :rule-classes :rewrite)
Theorem:
(defthm vl-match-always-at-some-edges-of-vl-stmt-fix-x (equal (vl-match-always-at-some-edges (vl-stmt-fix x)) (vl-match-always-at-some-edges x)))
Theorem:
(defthm vl-match-always-at-some-edges-vl-stmt-equiv-congruence-on-x (implies (vl-stmt-equiv x x-equiv) (equal (vl-match-always-at-some-edges x) (vl-match-always-at-some-edges x-equiv))) :rule-classes :congruence)