Question

In the following abstract grammars, b denotes a boolean expression, v denotes a local variable name, and e denotes an expression.

The abstract grammar for unclocked sequences is R

R ::= b // "boolean expression" form
| ( 1, v = e ) // "local variable sampling" form
| ( R ) // "parenthesis" form
| ( R ##1 R ) // "concatenation" form
| ( R ##0 R ) // "fusion" form
| ( R or R ) // "or" form
| ( R intersect R ) // "intersect" form
| first_match ( R ) // "first match" form
| R [ *0 ] // "null repetition" form
| R [ *1:$ ] // "unbounded repetition" form

The abstract grammar for clocked sequences is

S ::= @(b) R // "clock" form
| ( S ) // "parenthesized" form
| ( S ## S ) // "concatenation" form

The abstract grammar for unclocked properties is

P ::= R // "sequence" form
| ( P ) // "parenthesis" form
| not P // "negation" form
| ( P or P ) // "or" form
| ( P and P ) // "and" form
| ( R |-> P ) // "implication" form
| disable iff ( b ) P // "reset" form

Each instance of R in this production must be a non-degenerate unclocked sequence. In the “sequence” form, R must not be tightly satisfied by the empty word. See H.3.2 and H.3.5 for the definitions of non-degeneracy and tight satisfaction.

The abstract grammar for clocked properties is

Q ::= @( b ) P // "clock" form
| S // "sequence" form
| ( Q ) // "parenthesis" form
| not Q // "negation" form
| ( Q or Q ) // "or" form
| ( Q and Q ) // "and" form
| ( S |-> Q ) // "implication" form
| disable iff ( b ) Q // "reset" form

Each instance of S in this production must be a non-degenerate clocked sequence. In the “sequence” form, S must not be tightly satisfied by the empty word. See H.3.2 and H.3.5 for the definitions of non-degeneracy and tight satisfaction.

The abstract grammar for assertions is

A ::= always assert property Q // "always" form
| always @( b ) assert property P // "always with clock" form
| initial assert property Q // "initial" form
| initial @( b ) assert property P // "initial with clock" form