Section G.1

LRM-130

Change (changes in red and blue):

b)       The abstract syntax eliminates instantiation of sequences and properties. The semantics of an assertion with an instance of a sequence or non-recursive property is the same as the semantics of a related assertion obtained by replacing the sequence or non-recursive property instance with an explicitly written sequence or property. The explicit sequence or property is obtained from the body of the associated declaration by substituting actual arguments for formal arguments. A separate section defines the semantics of instances of recursive properties in terms of the semantics of instances of non-recursive properties.

LRM-130

Change (changes in red and blue):

 

d) The abstract syntax does not allow explicit procedural enabling conditions for assertions. Procedural enabling conditions are utilized in the semantics definition (see Subsection 3.3.1), but the method for extracting such conditions is not defined in this appendix.

 

4)       The abstract syntax eliminates the distinction between property_expr and property_spec from the full BNF.  Without the distinction, disable iff is a general, nestable property-building operator, while in the full BNF disable iff can be attached only at the top level of a property.  Semantically, there is no need for this restriction on the placement of disable iff.  The abstract syntax thus eliminates an unnecessary semantic layer while maintaining the simple inductive form for the definition of the semantics of properties.  As a result, semantics are given for some properties that do not correspond to forms from the full BNF, but this does not degrade the definitions for the properties that do correspond to forms from the full BNF.

LRM-130 LRM-131

Change (changes in red and blue):

In order to use this appendix to determine the semantics of a SystemVerilog assertion, the assertion must first be transformed into an enabling condition together with an assertion in the abstract syntax. This For assertions that do not involve recursive properties, this transformation involves eliminating sequence and non-recursive property instances by substitution, eliminating local variable declarations, introducing parentheses, determining the enabling condition, determining implicit or inferred clocking event controls, and eliminating redundant clocking event controls. For example, the following SystemVerilog assertion

LRM-130

Change (changes in red and blue):

is transformed into the enabling condition “b” together with the assertion

 

always @(c) assert property ((A ##1 B) |=> (A[*1:2] ##1 B))

 

in the abstract syntax.

 

If the SystemVerilog assertion involves instances of recursive properties, then the transformation replaces these instances with placeholder functions of the actual arguments.  The semantics of an instance of a recursive property is defined in terms of associated non-recursive properties in Section G.5.  Once the semantics of the recursive property instances are understood, the placeholder functions are treated as properties with these semantics.  Then the ordinary definitions can be applied to the transformed assertion in the abstract syntax together with placeholder functions.

Section G.2.1

LRM-131

Change (changes in red and blue):

The abstract grammar for unclocked properties is

P ::= [disable iff ( b )] [not] R                                      // "sequence" form

   | [disable iff ( b )] [not] ( R |-> [not] R )  // "implication" form

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.See G.3.2 and G.3.5 for the definition of non-degeneracy.

 

The abstract grammar for clocked properties is

Q ::= @(b) P // "clock" form

        | [disable iff ( b )] [not] S                                         // "sequence" form

        | [disable iff ( b )] [not] ( S |-> [not] S )      // "implication" form

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

Section G.2.2

LRM-131

Change (changes in red and blue):

The following auxiliary notions will be used in defining the semantics.

 

• j is an unclocked property fragment provided “disable iff (b) j”  is an unclocked property.

 

• N is a negation specifier if N is either the empty token or not.

 

Throughout the sequel, the following notational conventions will be used: b, c denote boolean expressions; v denotes a local variable name; e denotes an expression; j denotes an unclocked property fragment; N, N1, N2 denote negation specifiers; R, R1, R2 denote unclocked sequences; S, S1, S2 denote clocked sequences; P denotes an unclocked property; Q denotes a clocked property; A denotes an assertion; i, j, k, m, n denote non-negative integer constants.

Section G.2.3.1

LRM-131

Change (changes in red and blue):

• ( R1 |=> N R2 P) º ((R1 ##1 1 ) |-> N R2 P ) .

• ( S1 |=> N S2 Q) º ((S1 ## @(1) 1 ) |-> N S2 Q ) .

Section G.2.3.5

LRM-129

Change (changes in red and blue):

• ( b R, v = e ) º ( b R ##0 ( 1, v = e )) .

 

• ( b R, v1 = e1,... ,vk = ek) º (( b R, v1 = e1) ##0 ( 1, v2 = e2 ,... , vk = ek )) for k > 1.

LRM-131

Change (changes in red and blue):

• ( b, v1 = e1,... ,vk = ek) º (( b, v1 = e1) ##0 ( 1, v2 = e2 ,... , vk = ek )) for k > 1.

 

·         (if (b) P) º (b |-> P)

 

·         (if (b) P1 else P2) º ((b |-> P1) and (!b |-> P2))

Section G.3.1

LRM-131

Change (changes in red and blue):

• @(c)(R P ) ® (@(c) R P) .

LRM-131

Change (changes in red and blue):

• @(c) disable iff ( b ) j P  ® disable iff ( b ) @(c) j P.

 

• @(c) not b @(c) ® !b .

 

• @(c) not R P ® not @(c) R P, provided R is not a boolean expression.

 

• @(c) N1 ( R1 |-> N2 R2 P) º® N1( @(c) R1 |-> @(c) N2 R2 P) .

 

• ( S1 ## S2 ) ® ( S1 ##1 S2 ) .

 

·         @(c) (P1 or P2)  ®  (@(c) P1 or @(c) P2).

 

·         @(c) (P1 and P2)  ®  (@(c) P1 and @(c) P2).

Section G.3.3.1

LRM-131

Change (changes in red and blue):

Neutral satisfaction of properties:

 

• w |= (P ) iff w |= P

 

• w |= Q iff w  |= Q’, where Q’ is the unclocked property that results from Q by applying the rewrite rules.

 

• w |= disable iff (b) j P iff either w |= j P  or there exists 0 £  k < |w| such that w k |= b and w 0, k–1 Tw |= j P. Here, w 0, –1 denotes the empty word.

 

• w |= not j P  iff Ø(w |= j P).

 

• w |= R iff there exists 0 £ j < |w| such that w 0, j  |=R .

 

• w |= ( R1 |-> N R2 P) iff for every 0 £ j < |w| such that w 0, j |==R1, w j.. |= N R2 P .

 

·         w |= (P1 or P2) iff w |= P1 or w |= P2.

 

·         w |= (P1 and P2) iff w |= P1 and w |= P2.

Section G.3.6.1

LRM-131

Change (changes in red and blue):

• w, L0 |= disable iff (b) j P  iff either w, L0 |= j P  or there exists 0 £ k < |w| such that w k |= b[L0] and w 0, k–1 Tw, L0  |= j P. Here, w 0, –1 denotes the empty word.

 

• w, L0 |= not j P  iff w, L0 |=  j P  .

 

• w, L0 |= R iff there exist 0 £ j < |w| and L1 such that w 0, j, L0, L1 |= R .

 

• w, L0 |= ( R1 |-> N R2 P) iff for every 0 £ j < |w| and L1 such that w 0, j, L0, L1 R1, w j.., L1 N R2 P .

 

·         w,L0 |= (P) iff  w,L0 |= P.

 

·         w,L0 |= (P1 or P2) iff w,L0 |= P1 or w,L0 |= P2.

 

·         w,L0 |= (P1 and P2) iff w,L0 |= P1 and w,L0 |= P2.

Section G.4.1

LRM-128

Change (changes in red and blue):

w denotes a non-empty finite or infinite word over S, j denotes an integer such that 0 £ j < |w|, and T(V) denotes an instance of a clocked or unclocked sequence that is passed the local variables V as actual arguments.

 

·          w j,L0,L1 |= |== T(V).ended iff there exist 0 £ i £ j and L such that both w i, j, {}, L |== T(V) and L1 = L0 |D È L|V , where D = dom(L0) - (dom(L) Ç V) .

 

·         w j,L0,L1 |= @(c)(T(V).matched) iff there exists 0 £ i < j such that w i,L0,L1|= T(V).ended and w i+1, j , {}, {} |== (!c [*0:$] ##1 c) .

Section G.5 (New)

LRM-130

Change (changes in red and blue):

G.5  Recursive Properties

This section defines the neutral semantics of instances of recursive properties in terms of the neutral semantics of instances of non-recursive properties.  The latter can be expanded to properties in the abstract syntax by appropriate substitutions, and so their semantics is assumed to be understood.

 

According to Restriction 1 in Section 17.10.1, it is understood below that the negation operator not cannot be applied to any property expression that instantiates a recursive property.  Restriction 2 in Section 17.10.1 is not represented here because disable iff is treated as a general property-building operator in this appendix.  A precise version of Restriction 3 is given below.

 

Defined property p is said to depend on defined property q if there exist n ³ 0 and defined properties p0,...,pn such that p0 = p, pn = q, and for all 0 £ i < n, the definition of property pi instantiates property pi+1.  In particular, by taking q = p and n = 0, it follows that property p depends on property p.

 

A defined property p has an associated dependency digraph.  The nodes of the digraph are all the defined properties on which p depends.  If q and r are nodes of the digraph, then there is an arc from q to r for each instance of r in the definition of q.  Such an arc is labelled by the minimum number of timesteps that are guaranteed from the beginning of the definition of q until the particular instance r.  For example, if q is defined

by

 

property q;

   (a |-> r)

   and

   ((b ##1 c[*0:3]) |=> r);

endproperty

 

where a, b, c are boolean expressions, then there is one arc from q to r labeled by "0" due to a |-> r and there is a second arc from q to r labeled by "2" due to (b ##1 c[*0:3]) |=> r.

 

A defined property p is called recursive if its node appears on a cycle in the dependency digraph of p. 

 

The following is a precise version of Restriction 3:

 

RESTRICTION 3:  The sum of the arc labels around any cycle of the dependency digraph of a recursive property must be positive.

 

Let p(X) be an instance of a recursive defined property p, where X denotes the actual arguments of the instance.  For k ³ 0, the k-fold approximation to p(X), denoted p[k](X), is an instance of a non-recursive property p[k] defined inductively as follows.

 

·         The definition of p[0] is obtained from the definition of p by replacing the body property_expr with the literal 1’b1.

 

·         For k > 0, the definition of p[k] is obtained from the definition of p by replacing each instance of a recursive property by its (k - 1)-fold approximation.

 

The semantics of the instance p(X) is then defined as follows. For any word w over S and local variable context L, w,L |= p(X) iff for all k ³ 0, w,L |= p[k](X).