(vl-clkdecl-condcheck! x) → warnings
Function:
(defun vl-clkdecl-condcheck! (x) (declare (xargs :guard (vl-clkdecl-p x))) (let ((__function__ 'vl-clkdecl-condcheck!)) (declare (ignorable __function__)) (b* (((vl-clkdecl x) (vl-clkdecl-fix x))) (b* ((warnings ((lambda (x) (vl-evatomlist-condcheck x nil)) x.event)) (warnings1 (vl-maybe-clkskew-condcheck! x.iskew)) (warnings (vl-warningtree-cons warnings1 warnings)) (warnings1 (vl-maybe-clkskew-condcheck! x.oskew)) (warnings (vl-warningtree-cons warnings1 warnings)) (warnings1 (vl-clkassignlist-condcheck! x.clkassigns)) (warnings (vl-warningtree-cons warnings1 warnings)) (warnings1 (vl-propertylist-condcheck! x.properties)) (warnings (vl-warningtree-cons warnings1 warnings)) (warnings1 (vl-sequencelist-condcheck! x.sequences)) (warnings (vl-warningtree-cons warnings1 warnings)) (warnings1 ((lambda (x) (vl-atts-condcheck x nil)) x.atts)) (warnings (vl-warningtree-cons warnings1 warnings))) warnings))))
Theorem:
(defthm vl-warningtree-p-of-vl-clkdecl-condcheck! (b* ((warnings (vl-clkdecl-condcheck! x))) (vl-warningtree-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-clkdecl-condcheck!-of-vl-clkdecl-fix-x (equal (vl-clkdecl-condcheck! (vl-clkdecl-fix x)) (vl-clkdecl-condcheck! x)))
Theorem:
(defthm vl-clkdecl-condcheck!-vl-clkdecl-equiv-congruence-on-x (implies (vl-clkdecl-equiv x x-equiv) (equal (vl-clkdecl-condcheck! x) (vl-clkdecl-condcheck! x-equiv))) :rule-classes :congruence)