		Search-engine friendly clone of the ACL2 documentation.

Stmtrewrite

Vl-waitstmt-rewrite

Convert wait statements into empty while loops.

Signature
(vl-waitstmt-rewrite condition body atts) → stmt
Arguments: condition — Guard (vl-expr-p condition).; 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:

wait (condition) body
  -->
begin
  while(condition)
    ; // this is just a null statement
  body
end

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 wait statement, perhaps simplifying the target language for later transforms to implement.

BOZO is this sound? Can we come up with some tests that establish it is valid? What if the condition is X/Z?

Definitions and Theorems

Function: vl-waitstmt-rewrite

(defun vl-waitstmt-rewrite (condition body atts)
 (declare (xargs :guard (and (vl-expr-p condition)
                             (vl-stmt-p body)
                             (vl-atts-p atts))))
 (let ((__function__ 'vl-waitstmt-rewrite))
   (declare (ignorable __function__))
   (b* ((null (make-vl-nullstmt))
        (while (make-vl-whilestmt :condition condition
                                  :body null
                                  :atts (acons "VL_WAIT" nil atts)))
        (block (make-vl-blockstmt :sequentialp t
                                  :stmts (list while body))))
     block)))

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

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