		Search-engine friendly clone of the ACL2 documentation.

Stmtrewrite

Vl-foreverstmt-rewrite

Convert forever statements into while loops.

Signature
(vl-foreverstmt-rewrite body atts) → stmt
Arguments: body — Guard (vl-stmt-p body).; atts — Guard (vl-atts-p atts).
Returns: stmt — Type (vl-stmt-p stmt), given the guard.

The basic rewrite this performs is:

forever body
  -->
while(1)
  body

This might not be a very useful thing to do. It seems hard to synthesize arbitrary while loops. On the other hand, it does eliminate any forever statement, simplifying the target language for later transforms to implement.

Definitions and Theorems

Function: vl-foreverstmt-rewrite

(defun vl-foreverstmt-rewrite (body atts)
 (declare (xargs :guard (and (vl-stmt-p body)
                             (vl-atts-p atts))))
 (let ((__function__ 'vl-foreverstmt-rewrite))
  (declare (ignorable __function__))
  (b*
   ((const-one (make-vl-constint :origwidth 1
                                 :origtype :vl-unsigned
                                 :value 1))
    (atom-one (make-vl-atom :guts const-one))
    (while (make-vl-whilestmt :condition atom-one
                              :body body
                              :atts (acons "VL_FOREVER" nil atts))))
   while)))

Theorem: vl-stmt-p-of-vl-foreverstmt-rewrite

(defthm vl-stmt-p-of-vl-foreverstmt-rewrite
  (implies (and (force (vl-stmt-p body))
                (force (vl-atts-p atts)))
           (b* ((stmt (vl-foreverstmt-rewrite body atts)))
             (vl-stmt-p stmt)))
  :rule-classes :rewrite)