		Search-engine friendly clone of the ACL2 documentation.

Stmtrewrite

Vl-repeatstmt-rewrite

Unroll deterministic repeat statements.

Signature
(vl-repeatstmt-rewrite condition body atts warnings unroll-limit) → (mv warnings stmt)
Arguments: condition — Guard (vl-expr-p condition).; body — Guard (vl-stmt-p body).; atts — Guard (vl-atts-p atts).; warnings — Guard (vl-warninglist-p warnings).; unroll-limit — Guard (natp unroll-limit).
Returns: warnings — Type (vl-warninglist-p warnings), given the guard.; stmt — Type (vl-stmt-p stmt), given the guard.

The basic rewrite this performs is:

repeat(n) body;   // with 0 <= n <= unroll-limit
  -->
begin
  body   }
  body   }  n times
  ...    }
  body   }
end

We only try to unroll when n is easily resolved to a constant that is less than the unroll-limit. In particular, we use vl-consteval to try to evaluate the condition. This lets us handle things like repeat(width-1) body after unparameterization has occurred.

Definitions and Theorems

Function: vl-repeatstmt-rewrite

(defun vl-repeatstmt-rewrite
       (condition body atts warnings unroll-limit)
 (declare (xargs :guard (and (vl-expr-p condition)
                             (vl-stmt-p body)
                             (vl-atts-p atts)
                             (vl-warninglist-p warnings)
                             (natp unroll-limit))))
 (let ((__function__ 'vl-repeatstmt-rewrite))
  (declare (ignorable __function__))
  (b* (((mv ok count-expr)
        (vl-consteval condition nil))
       (count (and ok (vl-resolved->val count-expr)))
       ((when (and count (<= count unroll-limit)))
        (mv warnings
            (make-vl-blockstmt
                 :sequentialp t
                 :stmts (replicate count body)
                 :atts (acons "VL_UNROLL_REPEAT" nil atts)))))
   (mv
    (warn
     :type :vl-unroll-fail :msg
     (if count
      "Cannot unroll repeat statement because the count, ~
                         ~a0, did not resolve to a constant."
      "Cannot unroll repeat statement because the count, ~a0, ~
                       resolevd to ~x1, which exceeds the unroll limit of ~x2.")
     :args (list condition count unroll-limit))
    (make-vl-repeatstmt
         :condition condition
         :body body
         :atts (acons "VL_UNROLL_REPEAT_FAIL" nil atts))))))

Theorem: vl-warninglist-p-of-vl-repeatstmt-rewrite.warnings

(defthm vl-warninglist-p-of-vl-repeatstmt-rewrite.warnings
 (implies
     (and (force (vl-expr-p condition))
          (force (vl-stmt-p body))
          (force (vl-atts-p atts))
          (force (vl-warninglist-p warnings))
          (force (natp unroll-limit)))
     (b* (((mv ?warnings ?stmt)
           (vl-repeatstmt-rewrite condition
                                  body atts warnings unroll-limit)))
       (vl-warninglist-p warnings)))
 :rule-classes :rewrite)

Theorem: vl-stmt-p-of-vl-repeatstmt-rewrite.stmt

(defthm vl-stmt-p-of-vl-repeatstmt-rewrite.stmt
 (implies
     (and (force (vl-expr-p condition))
          (force (vl-stmt-p body))
          (force (vl-atts-p atts))
          (force (vl-warninglist-p warnings))
          (force (natp unroll-limit)))
     (b* (((mv ?warnings ?stmt)
           (vl-repeatstmt-rewrite condition
                                  body atts warnings unroll-limit)))
       (vl-stmt-p stmt)))
 :rule-classes :rewrite)