Maybe install an outer block name like
Either way we still create a
Function:
(defun vl-maybe-inject-block-name-into-assertion (name stmt) (declare (xargs :guard (and (stringp name) (vl-stmt-p stmt)))) (let ((__function__ 'vl-maybe-inject-block-name-into-assertion)) (declare (ignorable __function__)) (vl-stmt-case stmt :vl-assertstmt (change-vl-assertstmt stmt :assertion (change-vl-assertion stmt.assertion :name name)) :vl-cassertstmt (change-vl-cassertstmt stmt :cassertion (change-vl-cassertion stmt.cassertion :name name)) :otherwise (vl-stmt-fix stmt))))
Theorem:
(defthm vl-stmt-p-of-vl-maybe-inject-block-name-into-assertion (b* ((new-stmt (vl-maybe-inject-block-name-into-assertion name stmt))) (vl-stmt-p new-stmt)) :rule-classes :rewrite)