Wrapper for vl-stmt-rewrite that adds additional rewrites that are valid only for top-level statements.
(vl-stmt-rewrite-top x unroll-limit warnings) → (mv warnings new-x)
Beyond the ordinary rewrites, we carry out:
@(...) nullstmt --> nullstmt
This isn't valid in general, because, e.g., a sequence such as:
a = b; @(posedge clk) ; // nullstmt is here a = c;
is much different than just doing the assignments sequentially. But if we
have a whole
Function:
(defun vl-stmt-rewrite-top (x unroll-limit warnings) (declare (xargs :guard (and (vl-stmt-p x) (natp unroll-limit) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-stmt-rewrite-top)) (declare (ignorable __function__)) (b* (((mv warnings x) (vl-stmt-rewrite x unroll-limit warnings)) ((when (and (vl-timingstmt-p x) (vl-nullstmt-p (vl-timingstmt->body x)))) (mv warnings (make-vl-nullstmt)))) (mv warnings x))))
Theorem:
(defthm vl-warninglist-p-of-vl-stmt-rewrite-top.warnings (implies (and (force (vl-stmt-p x)) (force (natp unroll-limit)) (force (vl-warninglist-p warnings))) (b* (((mv ?warnings ?new-x) (vl-stmt-rewrite-top x unroll-limit warnings))) (vl-warninglist-p warnings))) :rule-classes :rewrite)
Theorem:
(defthm vl-stmt-p-of-vl-stmt-rewrite-top.new-x (implies (and (force (vl-stmt-p x)) (force (natp unroll-limit)) (force (vl-warninglist-p warnings))) (b* (((mv ?warnings ?new-x) (vl-stmt-rewrite-top x unroll-limit warnings))) (vl-stmt-p new-x))) :rule-classes :rewrite)