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.
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.
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
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.
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
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.
• ( R1 |=> N R2 P) º ((R1 ##1 1 ) |-> N R2 P ) .
• ( S1 |=> N S2N S2
• ( 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.
• ( 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))
• @(c)(R P ) ® (@(c) R P) .
• @(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).
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 R21,
w j.. |= N R2
·
w |= (P1 or P2) iff w |= P1
or w |= P2.
·
w |= (P1 and P2) iff w |= P1 and w |= P2.
• 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 R21, w j.., L1 N R2
·
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.
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