We just support null statements and blocking assignments.
Function:
(defun vl-atomicstmt-cblock-p (x) (declare (xargs :guard (vl-stmt-p x))) (declare (xargs :guard (vl-atomicstmt-p x))) (let ((__function__ 'vl-atomicstmt-cblock-p)) (declare (ignorable __function__)) (case (vl-stmt-kind x) (:vl-nullstmt t) (:vl-assignstmt (and (eq (vl-assignstmt->type x) :vl-blocking) (not (vl-assignstmt->ctrl x)) (vl-idexpr-p (vl-assignstmt->lvalue x)) (vl-expr->finaltype (vl-assignstmt->lvalue x)) (vl-expr->finaltype (vl-assignstmt->expr x)) (posp (vl-expr->finalwidth (vl-assignstmt->lvalue x))) (posp (vl-expr->finalwidth (vl-assignstmt->expr x))))) (otherwise nil))))
Theorem:
(defthm booleanp-of-vl-atomicstmt-cblock-p (b* ((bool (vl-atomicstmt-cblock-p x))) (booleanp bool)) :rule-classes :type-prescription)