		Search-engine friendly clone of the ACL2 documentation.

Vl-stmt

Vl-waitstmt

Representation of wait statements.

This is a product type, introduced by deftagsum in support of vl-stmt.

Fields

condition — vl-expr
body — vl-stmt
atts — vl-atts

General Form:

wait (<condition>)
   <body>

See Section 9.7.6 (page 136). The wait statement first evaluates condition. If the result is true, body is executed. Otherwise, this flow of execution blocks until condition becomes 1, at which point it resumes and body is executed. There is no discussion of what happens when the condition is X or Z. I would guess it is treated as 0 like in if statements, but who knows.

Subtopics

Vl-waitstmt->condition: Get the condition field from a vl-waitstmt.
Make-vl-waitstmt: Basic constructor macro for vl-waitstmt structures.
Vl-waitstmt->body: Get the body field from a vl-waitstmt.
Vl-waitstmt->atts: Get the atts field from a vl-waitstmt.
Change-vl-waitstmt: Modifying constructor for vl-waitstmt structures.