Separate always blocks into supported combinational blocks and others.
(vl-filter-cblocks x vars scary warnings) → (mv cblocks others warnings)
Function:
(defun vl-filter-cblocks (x vars scary warnings) (declare (xargs :guard (and (vl-alwayslist-p x) (vl-vardecllist-p vars) (string-listp scary) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-filter-cblocks)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil (ok))) ((mv okp warnings) (vl-always-check-cblock (car x) vars scary warnings)) ((mv cblocks others warnings) (vl-filter-cblocks (cdr x) vars scary warnings))) (if okp (mv (cons (car x) cblocks) others warnings) (mv cblocks (cons (car x) others) warnings)))))
Theorem:
(defthm vl-alwayslist-p-of-vl-filter-cblocks.cblocks (implies (force (vl-alwayslist-p x)) (b* (((mv ?cblocks ?others ?warnings) (vl-filter-cblocks x vars scary warnings))) (vl-alwayslist-p cblocks))) :rule-classes :rewrite)
Theorem:
(defthm vl-alwayslist-p-of-vl-filter-cblocks.others (implies (force (vl-alwayslist-p x)) (b* (((mv ?cblocks ?others ?warnings) (vl-filter-cblocks x vars scary warnings))) (vl-alwayslist-p others))) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-filter-cblocks.warnings (b* (((mv ?cblocks ?others ?warnings) (vl-filter-cblocks x vars scary warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)