(vl-modelement-condcheck! x) → warnings
Function:
(defun vl-modelement-condcheck! (x) (declare (xargs :guard (vl-modelement-p x))) (let ((__function__ 'vl-modelement-condcheck!)) (declare (ignorable __function__)) (let ((x (vl-modelement-fix x))) (common-lisp::case (tag x) ((:vl-portdecl) (b* ((warnings ((lambda (x) (vl-portdecl-condcheck x nil)) x))) warnings)) ((:vl-assign) (b* ((warnings (vl-assign-condcheck! x))) warnings)) ((:vl-alias) (b* ((warnings (vl-alias-condcheck! x))) warnings)) ((:vl-vardecl) (b* ((warnings ((lambda (x) (vl-vardecl-condcheck x nil)) x))) warnings)) ((:vl-paramdecl) (b* ((warnings ((lambda (x) (vl-paramdecl-condcheck x nil)) x))) warnings)) ((:vl-fundecl) (b* ((warnings (vl-fundecl-condcheck! x))) warnings)) ((:vl-taskdecl) (b* ((warnings (vl-taskdecl-condcheck! x))) warnings)) ((:vl-modinst) (b* ((warnings (vl-modinst-condcheck! x))) warnings)) ((:vl-gateinst) (b* ((warnings (vl-gateinst-condcheck! x))) warnings)) ((:vl-always) (b* ((warnings (vl-always-condcheck! x))) warnings)) ((:vl-initial) (b* ((warnings (vl-initial-condcheck! x))) warnings)) ((:vl-final) (b* ((warnings (vl-final-condcheck! x))) warnings)) ((:vl-typedef) (b* ((warnings ((lambda (x) (vl-typedef-condcheck x nil)) x))) warnings)) ((:vl-import) (b* ((warnings ((lambda (x) (vl-import-condcheck x nil)) x))) warnings)) ((:vl-fwdtypedef) (b* ((warnings (vl-fwdtypedef-condcheck! x))) warnings)) ((:vl-modport) (b* ((warnings (vl-modport-condcheck! x))) warnings)) ((:vl-genvar) (b* ((warnings (vl-genvar-condcheck! x))) warnings)) ((:vl-assertion) (b* ((warnings ((lambda (x) (vl-assertion-condcheck x nil)) x))) warnings)) ((:vl-cassertion) (b* ((warnings ((lambda (x) (vl-cassertion-condcheck x nil)) x))) warnings)) ((:vl-property) (b* ((warnings (vl-property-condcheck! x))) warnings)) ((:vl-sequence) (b* ((warnings (vl-sequence-condcheck! x))) warnings)) ((:vl-clkdecl) (b* ((warnings (vl-clkdecl-condcheck! x))) warnings)) ((:vl-gclkdecl) (b* ((warnings (vl-gclkdecl-condcheck! x))) warnings)) ((:vl-defaultdisable) (b* ((warnings (vl-defaultdisable-condcheck! x))) warnings)) ((:vl-dpiimport) (b* ((warnings (vl-dpiimport-condcheck! x))) warnings)) ((:vl-dpiexport) (b* ((warnings (vl-dpiexport-condcheck! x))) warnings)) ((:vl-bind) (b* ((warnings (vl-bind-condcheck! x))) warnings)) ((:vl-class) (b* ((warnings (vl-class-condcheck! x))) warnings)) ((:vl-covergroup) (b* ((warnings (vl-covergroup-condcheck! x))) warnings)) ((:vl-elabtask) (b* ((warnings (vl-elabtask-condcheck! x))) warnings)) (otherwise (b* ((warnings ((lambda (x) (vl-letdecl-condcheck x nil)) x))) warnings))))))
Theorem:
(defthm vl-warningtree-p-of-vl-modelement-condcheck! (b* ((warnings (vl-modelement-condcheck! x))) (vl-warningtree-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-modelement-condcheck!-of-vl-modelement-fix-x (equal (vl-modelement-condcheck! (vl-modelement-fix x)) (vl-modelement-condcheck! x)))
Theorem:
(defthm vl-modelement-condcheck!-vl-modelement-equiv-congruence-on-x (implies (vl-modelement-equiv x x-equiv) (equal (vl-modelement-condcheck! x) (vl-modelement-condcheck! x-equiv))) :rule-classes :congruence)