The variables that can
appear in expressions must be static design variables or function calls returning
values of types described in Section 17.4.1. The
functions should be automatic (or preserve no state information) and pure (no
output arguments, no side effects). Static variables declared in
programs, interfaces or clocking domains blocks can also be accessed. If a reference is to a
static variable declared in a task, that variable is sampled as any other
variable, independent of calls to the task.
sequence_expr ::= // from Annex A.2.10
cycle_delay_range sequence_expr { cycle_delay_range sequence_expr }
| sequence_expr
cycle_delay_range sequence_expr { cycle_delay_range
sequence_expr }
| expression expression_or_dist { , variable_assignment } [ boolean_abbrev ]
| ( expression expression_or_dist
{, variable_assignment } ) [ boolean_abbrev ]
|
sequence_instance [ sequence_abbrev ]
| ( sequence_expr {, variable_assignment } ) [ sequence_abbrev ]
| sequence_expr and sequence_expr
| sequence_expr intersect sequence_expr
| sequence_expr or sequence_expr
| first_match ( sequence_expr )
| expression throughout sequence_expr
| sequence_expr within sequence_expr
actual_arg_expr ::=
event_expression
| $
cycle_delay_const_range_expression ::=
constant_expression : constant_expression
| constant_expression : $
expression
| expression dist
{ dist_list }
— a clocking domain
block as a clocking_item
multi_clock_sequence::=
clocked_sequence
{ ## clocked_sequence }
sequence_expr
| clocking_event multi_clock_sequence
| ( multi_clock_sequence )
| multi_clock_sequence ## multi_clock_sequence
clocked_sequence ::=
clocking_event
sequence_expr
actual_arg_expr ::=
event_expression
| $
An actual argument
can replace an:
— identifier
— expression
— event control expression
— upper range as $
|
SystemVerilog
expression operators |
Associativity |
|
|
|
|
[*] [*=] [*->] |
|
|
## |
left |
|
|
|
|
|
left |
|
|
left |
|
|
left |
|
|
left |
sequence_expr ::= // from Annex A.2.10
…
| expression expression_or_dist { , variable_assignment } [ boolean_abbrev ]
| ( expression expression_or_dist
{, variable_assignment } ) [ boolean_abbrev ]
|
sequence_instance [ sequence_abbrev ]
| ( sequence_expr {, variable_assignment } ) [ sequence_abbrev ]
…
17.7.3
Value change Sampled
value functions
This section
describes the system functions available for accessing sampled values of an
expression. These functions include the capability to access current sampled value, access sampled value in the past, or detect changes
in sampled value of an expression. Sampling of an expression is explained in
Section 17.3. Following functions are provided.
Three functions
are provided to detect changes in values between two adjacent clock ticks: $rose, $fell and $stable.
$sampled(expression
[ , clocking_event])
$rose ( expression [ , clocking_event])
$fell ( expression [ , clocking_event])
$stable ( expression [ , clocking_event])
$past (expression1 [,number_of_ticks][,expression2][,clocking_event]
)
A value change
expression at a clock tick detects the change in value of an expression from
the value of that expression at the previous clock tick. The result of a value
change expression is true or false and can be used as a boolean
expression. At the first clock tick after the assertion is started, the result
of these functions are computed by comparing the current value to ‘x’.
The use of these
functions is not limited to assertion features; they can be used as expressions
in procedural code as well. The clocking event, although optional as an
explicit argument to the functions, is required for their semantics. The
clocking event is used to sample the value of the argument expression.
The clocking
event must be explicitly specified as an argument, or inferred from the code
where it is used. The following rules are used to infer the clocking event:
— if used in an assertion, the appropriate clocking event from
the assertion is used.
— if used in an action block of a singly clocked assertion,
the clock of the assertion is used.
— if used in a procedural block, the inferred clock, if any,
for the procedural code (Section 17.12.2) is used.
Otherwise,
default clocking (Section 15.11) is used.
When these
functions are used in an assertion, the clocking event argument of the
functions, if specified, shall be identical to the clocking event of the
expression in the assertion. In the case of multi-clock assertion, the
appropriate clocking event for the expression where the function is used, is applied to the function.
Function $sampled returns
the sampled value of the expression with respect to the last occurrence of the
clocking event. When $sampled is invoked prior to the occurrence of the
first clocking event, the value of X is returned. The use of $sampled in
assertions, although allowed, is redundant, as the result of the function is
identical to the sampled value of the expression itself used in the assertion.
Three functions
are provided to detect changes in sampled values: $rose, $fell and $stable.
A value change
function detects the change in the sampled value of an expression. The clocking
event is used to obtain the sampled value of the argument expression at a clock
tick prior to the current simulation time unit. Here, the current simulation
time unit refers to the simulation time unit in which the function is
evaluated. This sampled value is compared against the value of the expression
determined at the prepone time of the current simulation time unit. The result
of a value change expression is true or false and can be used as a boolean expression.
$rose returns
true if the least significant bit of the expression changed to 1. Otherwise, it
returns false.
$fell returns
true if the least significant bit of the expression changed to 0. Otherwise, it
returns false.
$stable returns
true if the value of the expression did not change. Otherwise, it returns
false.
When these
functions are used at the first clock tick, determined by the clocking event,
or before the first clock tick, the result of these functions are computed by
comparing the current sampled value of the expression to X.
Figure 17-3 illustrates two
examples of value changes:
— Value change expression e1 is defined as $rose(req)
— Value change expression e2 is defined as $fell(ack)
INSERT FIGURE 17-3
The clock ticks used for
sampling the variables are derived from the clock for the property, which is
different from the simulation ticks. Assume, for now, that this clock is
defined elsewhere. At clock tick 3, e1 occurs because the value of req at clock tick 2 was low and at clock tick 3, the value
is high. Similarly, e2 occurs
at clock tick 6 because the value of ack was sampled as high at clock tick 5 and sampled as low
at clock tick 6.
The example
below illustrates the use of $rose in SystemVerilog code outside assertions.
always @(posedge clk)
reg1 <= a & $rose(b);
In this example,
the clocking event (posedge
clk) is applied to $rose. $rose is true
whenever the sampled value of b changed to 1 from its sampled value at the the
previous tick of the clocking event.
In addition to
accessing value changes, the past values can be accessed with the $past function. The
following three optional arguments are provided:
expression2 is used as a
gating expression for the clocking event
number_of_ticks specifies the
number of clock ticks in the past
clocking_event specifies the
clocking event for sampling expression1
expression1 and expression2 can be
any expression allowed in assertions.
number_of_ticks must be one or
greater. If number_of_ticks is not specified, then it defaults to 1. $past returns the
sampled value of the expression that was present number_of_ticks
prior to the time of
evaluation of $past. A clock tick is based on clocking_event. If the specified clock tick in the past
is before the start of simulation, the returned value from the $past function is
a value of X.
The optional
argument clocking_event specifies the clock for the function. The rules governing the usage
of clocking_event are same as those described for the value change function.
When
intermediate optional arguments between two arguments are not needed, a comma
must be placed for each ommited argument. For example,
$past(in1, ,
enable);
Here, a comma is
specified to omit number_of_ticks. The default of one is used for the empty number_of_ticks argument.
Note that a comma for the ommited clocking_event argument is not needed, as it does not fall
within the specified arguments.
$past can be used in any System Verilog expression. An example is
shown below.
always @(posedge clk)
reg1 <= a & $past(b);
In this example,
the clocking event (posedge
clk) is applied to $past. $past is evaluated
in the current occurrence of (posedge clk), and
returns the value of b sampled at the previous occurrence of (posedge clk).
When expression2 is
specified, the sampling of expression is performed based on its clock gated
with expression2.
For example,
always @(posedge clk)
if (enable) q <= d;
always @(posedge clk)
assert (done |=> (out == $past(q, 2,enable)) ;
In this example,
the sampling of q for evaluating $past is based on the clocking expression
posedge clk iff enable
ended can be
used directly on sequences that do not have formal arguments. To use ended on a sequence with arguments, first define a
sequence without formal arguments that instantiates the sequence with actual
arguments. For example, For
example with the definitions
sequence e2(a,b,c);
@(posedge
sysclk) $rose(a) ##1 b ##1 c;
endsequence
sequence e2_instantiated;
e2(ready,proc1,proc2);
endsequence
sequence rule2;
@(posedge
sysclk) reset ##1 inst ##1 e2_instantiated.ended
e2(ready,proc1,proc2).ended ##1
branch_back;
endsequence
rule2 is
equivalent to rule2a below:
sequence e2_instantiated;
e2(ready,proc1,proc2);
endsequence
sequence rule2a;
@(posedge sysclk) reset ##1 inst ##1
e2_instantiated.ended ##1 branch_back;
endsequence
There are additional restrictions on
passing local variables into an instance of a sequence to which ended is
applied. See Section 17.8.
The implication construct
allows a user to monitor sequences properties based on satisfying some criteria. Most
common uses are to attach a precondition to a sequence, where the evaluation of
the sequence is based on the success of a condition.
property_expr ::=
…
| sequence_expr
|-> [ not ] sequence_expr property_expr
| sequence_expr
|=> [ not ] sequence_expr property_expr
multi_clock_property_expr ::=
…
|
multi_clock_sequence |-> multi_clock_property_expr
|
multi_clock_sequence |=> [ not ] multi_clock_sequence multi_clock_property_expr
…
This clause is used to
precondition monitoring of a sequence property expression and is allowed at the property
level. The result of the implication is either true or false. The left-hand
side operand sequence_expr is called the
antecedent, while the right-hand side operand sequence_expr property_expr
is called the consequent.
The following points should
be noted for |-> implication:
— antecedent sequence_expr can result in multiple successful sequences.
— From a given start point, the antecedent
sequence_expr can have zero, one, or more than one successful match.
—
If there is no
match of the antecedent sequence_expr from a
given start point, then evaluation of the implication
from that start point succeeds vacuously by returning and returns true.
— For each successful match of antecedent
sequence_expr, the consequent sequence_exp property_expr is separately evaluated,
beginning at the end point of the match. That is, the end point of matching
sequence from antecedent sequence_expr overlaps with start point of the consequent
sequence_expr. The end point of the
match of the antecedent sequence_expr is the start point of the
evaluation of the consequent property_expr.
— From a given start point, evaluation of the
implication succeeds and returns true iff for every match of the antecedent
sequence_expr beginning at the start point, the evaluation of the consequent
property_expr beginning at the endpoint of the match succeeds and returns true.
— All matches of antecedent sequence_expr must
satisfy consequent sequence_expr. The satisfaction of the consequent
sequence_expr means that there is at least one match of the sequence_expr.
— Nesting of implication is not allowed.
Two forms of
implication are provided: overlapped using operator |->, and
non-overlapped using operator |=>. For overlapped implication, if there is a
match for the antecedent sequence_expr, then the first element of the consequent
sequence_expr is evaluated on the same clock tick end point of the match is the start point of the evaluation of the
consequent property_expr. For non-overlapped implication, the first element of the consequent
sequence_expr is evaluated on the next clock tick start point of the evaluation of the consequent property_expr is the clock tick after
the end point of the match.
Therefore:
sequence_expr |=> [not] sequence_expr property_expr
is
equivalent to:
sequence_expr ##1 ‘true |-> [not]
sequence_expr property_expr
If not is
used on the consequent, the result of consequent sequence_expr is
reversed.
The use of
implication when multi-clock sequences and properties are
involved is explained in Section 17.11.
Generally, assertions are
associated with preconditions so that the checking is performed only under
certain specified conditions. As seen from the previous example, the |->
operator provides this capability to
specify preconditions with sequences that must be satisfied before continuing to match those sequences evaluating their consequent properties. The next
example modifies the preceding example to see the effect on the results of the
assertion by removing the precondition for the sequence
consequent. This is shown below, and
illustrated in Figure 17-15.
property p16;
(write_en & data_valid) ##0
(write_en && (retire_address[0:4]==addr))
[*2] |->
##[3:8] write_en
&& !data_valid &&(write_address[0:4]==addr);
endproperty
This property can be coded alternatively as
a nested implication:
property p16_nested;
(write_en & data_valid) |->
(write_en && (retire_address[0:4]==addr)) [*2] |->
##[3:8]
write_en && !data_valid && (write_address[0:4]==addr);
endproperty
sequence_expr ::= // from Annex A.2.10
…
| expression { , variable_assignment } [ boolean_abbrev
]
| ( expression expression_or_dist
{, variable_assignment } ) [ boolean_abbrev ]
| ( sequence_expr
{, variable_assignment }
) [ sequence_abbrev ]
…
The type of variable is explicitly
specified. The variable can be assigned anywhere in
the sequence and reassigned later in the sequence..
at the end point of any syntactic subsequence by placing the
subsequence, comma separated from the sampling assignment, in parentheses. For example, if in
a ##1 b[*->1] ##1 c[*2]
it is desired to sample x = e at the
match of b,
the sequence expression can be rewritten as
a ##1 (b[*->1], x = e) ##1
c[*2]
The local variable can be reassigned later
in the sequence, as in
a ##1 (b[*->1], x = e) ##1
(c[*2], x = x + 1)
For every attempt, a new copy of the variable is
created for the sequence. The variable value can be tested like any other
SystemVerilog variable.
To access a local variable
of a sub-sequence, a local variable must be declared and passed to the
instantiated sub-sequence through an argument. An example below illustrates
this usage.
sequence sub_seq2(lv);
a ##1 !a, lv = data_in
##1 !b*[0:$] ##1 b && (data_out == lv);
endsequence
sequence seq2;
int v1;
c ##1 sub_seq2(v1) ##1
(do1 == v1); // v1 is now bound to lv
endsequence
Local variables can be passed into an
instance of a defined sequence to which ended is applied and accessed in a
similar manner. For example
sequence seq2a;
int v1; c ##1
sub_seq2(v1).ended ##1 (do1 == v1); // v1 is now bound to lv
endsequence
There are additional restrictions when
passing local variables into an instance of a defined sequence to which ended is
applied:
1.
Local variables can be passed in only as entire actual arguments, not as proper subexpressions of
actual arguments.
2.
In the declaration of the defined sequence, the formal argument to
which the local variable is bound must not be referenced before it is sampled.
The second restriction is met by sub_seq2 because the sampling lv = data_in occurs before the reference to lv in data_out == lv.
If a local variable is sampled before being
passed into an instance of a defined sequence to which ended is applied, then the restrictions prevent
this sampled value from being visible within the defined sequence. The restrictions are important because the
use of ended means that there is no guaranteed
relationship between the point in time at which the local variable is sampled
outside the defined sequence and the beginning of the match of the instance.
A local variable that is passed in as
actual argument to an instance of a defined sequence to which ended is applied will flow out of the
application of ended to that instance provided both of the
following conditions are met:
1.
The local variable flows out of the end of the defined sequence
instance, as defined by the local variable flow rules for sequences. (See below and Annex G.)
2.
The application of ended to this instance is a maximal boolean expression. In other words, the application of ended cannot have negation or any
other expression operator applied to it.
Both conditions are satisfied by sub_seq2 and seq2a. Thus, in seq2a the value in v1 in the
comparison do1
== v1 is the value sampled
into lv in sub_seq2 by the
assignment lv
= data_in. However, in
sequence seq2b;
int v1; c ##1
!sub_seq2(v1).ended ##1 (do1 == v1); // v1 undefined
endsequence
the second condition is violated because of the
negation applied to sub_seq2(v1).ended.
Therefore, v1 does not flow out of the application of
ended to this instance, and so the reference to v1 in do1
== v1 is to an unsampled
variable.
In a single cycle, there can be multiple
matches of a sequence instance to which ended is applied,
and these matches can have different valuations of the local variables. The multiple matches are treated semantically
the same way as matching both disjuncts of an or
(see below). In other words, the thread
evaluating the instance to which ended is applied
will fork to account for such distinct local variable valuations.
In addition to
accessing values of signals at the time of evaluation of a boolean
expression, the past values can be accessed with the $past function.
$past ( expression
[ , number_of_ticks] )
The optional
argument number_of_ticks specifies the number of clock ticks in the
past. If number_of_ticks is not specified, then it defaults to 1. $past returns
the sampled value of the expression that was present number_of_ticks prior
to the time of evaluation of $past.
— a
clocking domain block
as a clocking_item
property_spec ::=
[clocking_event ] [ disable iff ] ( expression ) ] [ not ]
property_expr
| [ disable iff ( expression ) ] [ not ] multi_clock_property_expr
property_expr ::=
sequence_expr
| ( property_expr )
| not property_expr
| property_expr or property_expr
| property_expr and property_expr
| sequence_expr
|-> [ not ] sequence_expr property_expr
| sequence_expr
|=> [ not ] sequence_expr property_expr
| if ( expression ) property_expr [ else property_expr ]
| property_instance
| ( property_expr )
multi_clock_property_expr ::=
property_expr
| multi_clock_sequence
| clocking_event multi_clock_property_expr
| ( multi_clock_property_expr )
| not
multi_clock_property_expr
| multi_clock_property_expr or multi_clock_property_expr
| multi_clock_property_expr and multi_clock_property_expr
|
multi_clock_sequence |-> multi_clock_property_expr
|
multi_clock_sequence |=> [ not ] multi_clock_sequence multi_clock_property_expr
| if ( expression ) multi_clock_property_expr [ else multi_clock_property_expr
]
| property_instance
| ( multi_clock_property_expr )
The result of property evaluation
is either true or false. There are two kinds of property: sequence, and
implication. If the property is just a sequence, the result of a sequence for
every evaluation attempt is true or false. This is accomplished by implicitly
transforming sequence_expr to first_match(sequence_expr). That is, as soon as a match of sequence_expr is determined,
the result is considered to be true, and no other matches are required for that
evaluation attempt. However, if the property is an implication, then the
semantics of implication determine whether the property is true or false.
The disable iff clause allows asynchronous resets to be specified. For a particular
attempt, if the expression of the disable iff becomes true at any time during the
evaluation of the attempt, then the attempt for the property is considered to be
a success. Other attempts are not affected by the evaluation of the expression
for an attempt.
The not clause
states that the property_expr associated with the property must never
evaluate to true. Effectively, it negates property_expr. For each attempt,
property_expr results in either true or false,
based on whether there is a match for the sequence. The not clause
reverses the result of property_expr. It should be noted that there is
no complementation or any form of negation for the sequence in property_expr.
The result of property evaluation is either true or false. There
are seven kinds of properties: sequence, negation, disjunction, conjunction,
if-else, implication, and instantiation.
1.
A
property that is a sequence evaluates to true if and only if there is a match of the sequence. Since there is a match if and only if there
is a first match, evaluation of such a property is the same as implicitly
transforming its sequence_expr to first_match(sequence_expr). As soon as a match of sequence_expr is determined, the evaluation of the property is
considered to be true, and no other matches are required for that evaluation
attempt.
2.
A
property is a negation if it has the form
not property_expr
For each evaluation attempt of the
property, there is an evaluation attempt of property_expr. The keyword not states that the evaluation of the property
returns the opposite of the evaluation of the underlying property_expr. Thus, if property_expr evaluates
to true, then not property_expr
evaluates to false, and if property_expr
evaluates to false, then not property_expr
evaluates to true.
3.
A
property is a disjunction if it has the form
property_expr1 or property_expr2
The property evaluates to true if and only
if at least one of
property_expr1 and property_expr2 evaluates to true.
4.
A
property is a conjunction if it has the form
property_expr1 and property_expr2
The property evaluates to true if and only
if both property_expr1 and property_expr2 evaluate to true.
5.
A
property is an if-else if it has either the form
if (expression) property_expr1
or the form
if (expression) property_expr1 else property_expr2
A property of the first form evaluates to
true if and only if either expression evaluates to false or property_expr1
evaluates to true. A property of the
second form evaluates to true if and only if either expression evaluates to
true and property_expr1 evaluates to true or expression evaluates to false and
property_expr2 evaluates to true.
6.
A property
is an implication if it has either the form
sequence_expr |-> property_expr
or the form
sequence_expr |=> property_expr
The meaning of implications has already
been discussed in 17.7.11.
7.
An
instance of a defined property can be used as a property_expr or
property_spec. In general, the instance
is legal provided the body property_spec of the defined property can be
substituted in place of the instance, with actual arguments substitited for
formal arguments, and result in a legal property_expr or property_spec,
ignoring local variable declarations.
Thus, for example, if an instance of a defined property is used as a
property_expr operand for any property-building operator, then the defined
property must not have a disable iff clause.
Similarly, clock events in a defined property must conform to the rules
of multiple clock support when the property is instantiated in a property_expr
or property_spec that also involves other clock events.
The following table lists the property operators from highest to
lowest precedence and shows the associativity of the non-unary operators.
Table 17-2 Property operator precedence and
associativity
|
SystemVerilog
property operators |
Associativity |
|
not |
---- |
|
and |
left |
|
or |
left |
|
if…else |
right |
|
|-> |=> |
right |
A disable iff clause can be attached to a property_expr
to yield a property_spec
disable iff (expression) property_expr
The expression of the disable iff is called the reset expression. The disable iff clause allows asynchronous resets to be
specified. For an evaluation of the
property_spec, there is an evaluation of the underlying property_expr. If during that evaluation the reset
expression becomes true, then the overall evaluation of the property_spec is
true. Otherwise, the evalution of the
property_spec is the same as that of the property_expr. The reset expression is tested independently
for different evaluation attempts of the property_spec. Nesting of disable iff clauses, explicitly or through property
instantiations, is not allowed.
Property rule2 negates the result of the implication (a
|-> b ##1 c ##1 d) for every attempt. clkev specifies the
clock for the property.
property rule3;
@(posedge clk) a[*2] |-> ((##[1:3] c) or (d |=> e));
endproperty
Property rule3 says that if a holds and a also held last cycle, then either c must hold at some point 1 to three cycles
after the current cycle, or, if d holds in the
current cycle, then e must hold one
cycle later.
property rule4;
@(posedge clk) a[*2] |-> ((##[1:3] c) and (d |=> e));
endproperty
Property rule4 says that if a holds and a also held last cycle, then c must hold at some point 1 to three cycles
after the current cycle, and if d holds in the
current cycle, then e must hold one
cycle later.
property rule5;
@(posedge clk)
a ##1 (b ||
c)[*->1] |->
if (b)
(##1 d |-> e)
else // c
f ;
endproperty
Property rule5 has a followed by the first match of either b or c as its
antecedent. The consequent uses if-else
to split cases on which of b or c is matched first.
property rule6(x,y);
##1 x |-> y;
endproperty
property rule5a;
@(posedge clk)
a ##1 (b ||
c)[*->1] |->
if (b)
rule6(d,e)
else // c
f ;
endproperty
Property rule5a is equivalent to rule5, but
it uses an instance of rule6 as a
property expression.
17.10.1 Recursive properties
SystemVerilog allows recursive property
definitions. A defined property is
recursive if its declaration involves an instantiation of itself. Recursion provides a flexible framework for
coding properties to serve as ongoing assumptions, checkers, or coverage
monitors.
For example,
property prop_always(p);
p
and (1’b1 |=> prop_always(p));
endproperty
is a recursive property that says that the formal argument
property p must hold at
every cycle. This example is useful if
the ongoing requirement that property p hold applies
after a complicated triggering condition encoded in sequence s:
property p1(s,p);
s
|=> prop_always(p);
endproperty
As another example, the recursive property
property prop_weak_until(p,q);
q or (p and (1’b1 |=> prop_weak_until(p,q)));
endproperty
says that formal argument property p must hold at every cycle up to but not
including the first cycle at which formal argument property q holds.
Formal argument property q is not required
ever to hold, though. This example is
useful if p must hold at every cycle after a
complicated triggering condition encoded in sequence s, but the requirement on p is lifted by q:
property p2(s,p,q);
s
|=> prop_weak_until(p,q);
endproperty
More generally, several property definitions can be mutually recursive. For example
property check_phase1;
s1 |-> (phase1_prop and (1’b1 |=> check_phase2));
endproperty
property check_phase2;
s2 |-> (phase2_prop and (1’b1 |=> check_phase1));
endproperty
There are three restrictions on recursive property definitions.
RESTRICTION 1: The negation
operator not cannot be applied to any property expression that instantiates a
recursive property. In particular, the
negation of a recursive property cannot be asserted or used in defining another
property.
Here are examples of illegal property definitions that violate
Restriction 1:
property illegal_recursion_1(p);
not prop_always(not p);
endproperty
property illegal_recursion_2(p);
p
and (1’b1 |=> not illegal_recursion_2(p));
endproperty
RESTRICTION 2: The operator disable iff cannot be used in the definition of a
recursive property. This restriction is
consistent with the restriction that disable iff cannot be
nested.
Here is an example of an illegal property definition that violates
Restriction 2:
property illegal_recursion_3(p);
disable iff (b)
p
and (1’b1 |=>
illegal_recursion_3(p));
endproperty
The intent of illegal_recursion_3
can be written legally as
property legal_3(p);
disable iff (b) prop_always(p);
endproperty
since legal_3 is not a recursive property.
RESTRICTION 3: If p is a
recursive property, then, in the definition of p, every instance of p must
occur after a positive advance in time.
In the case of mutually recursive properties, all recursive instances must
occur after positive advances in time.
Here is an example of an illegal property definition that violates
Restriction 3:
property illegal_recursion_4(p);
p
and (1’b1 |->
illegal_recursion_4(p));
endproperty
If this form were legal, the recursion would be stuck in time,
checking p over and
over again at the same cycle.
Recursive properties can deal with complicated requirements, such
as those associated with varying numbers of data beats, out-of-order
completions, retries, etc. Here is an
example of using a recursive property to check complicated conditions of this
kind.
EXAMPLE: Suppose that write
data must be checked according to the following conditions:
·
Acknowledgment
of a write request is indicated by the signal write_request together with write_request_ack. When a write request is acknowledged, it gets
a 4-bit tag, indicated by signal write_reqest_ack_tag. The
tag is used to distinguish data beats for multiple write transactions in flight
at the same time.
·
It is
understood that distinct write transactions in flight at the same time must be
given distinct tags. For simplicity,
this condition is not a part of what is checked in this example.
·
Each
write transaction can have between 1 and 16 data beats, and each data beat is 8
bits. There is a model of the expected
write data that is available at acknowledgment of a write request. The model is a 128 bit vector. The most significant group of 8 bits
represents the expected data for the first beat, the next group of 8 bits
represents the expected data for the second beat (if there is a second beat),
and so forth.
·
Data
transfer for a write transaction occurs after acknowledgment of the write
request and, barring retry, ends with the last data beat. The data beats for a single write transaction
occur in order.
·
A data
beat is indicated by the data_valid signal
together with the signal data_valid_tag to
determine the relevant write transaction.
The signal data is valid with data_valid and carries the data for that beat. The data for each beat must be correct
according to the model of the expected write data.
·
The
last data valid is indicated by signal last_data_valid
together with data_valid and data_valid_tag. For simplicity, this example does not
represent the number of data beats and does not check that last_data_valid is signaled at the correct beat.
·
At any
time after acknowledgement of the write request, but not later than the cycle
after the last data valid, a write transaction can be forced to retry. Retry is indicated by the signal retry together with signal retry_tag to identify the relevant write
transaction. If a write transaction is
forced to retry, then its current data transfer is aborted and the entire data
transfer must be repeated. The transaction
does not re-request and its tag does not change.
·
There
is no limit on the number of times a write transaction can be forced to retry.
·
A
write transaction completes the cycle after the last data valid provided it is
not forced to retry in that cycle.
Here is code to check these conditions:
property check_write;
[0:127] expected_data; // local variable to sample model data
[3:0] tag; // local variable to sample tag
disable iff
(reset)
(
write_request && write_request_ack,
expected_data = model_data,
tag =
write_request_ack_tag
)
|=>
check_write_data_beat(expected_data,
tag, 4'h0);
endproperty
property check_write_data_beat
(
expected_data, // [0:127]
tag, // [3:0]
i // [3:0]
);
first_match
(
##[0:$]
(
(data_valid && (data_valid_tag
== tag))
||
(retry
&& (retry_tag == tag))
)
)
|->
(
(
(data_valid && (data_valid_tag
== tag)
|->
(data ==
expected_data[i*8+:8])
)
and
(
if (retry && (retry_tag == tag))
(
1’b1 |=> check_write_data_beat(tag, expected_data, 4’h0)
)
else if (!last_data_valid)
(
1’b1 |=> check_write_data_beat(tag, expected_data, i+4’h1)
)
else
(
##1 (retry && (retry_tag ==
tag))
|=>
check_write_data_beat(tag,
expected_data, 4'h0)
)
)
);
endproperty
multi_clock_sequence::=
clocked_sequence
{ ## clocked_sequence }
sequence_expr
| clocking_event multi_clock_sequence
| ( multi_clock_sequence )
| multi_clock_sequence ## multi_clock_sequence
clocked_sequence ::=
clocking_event
sequence_expr
multi_clock_property_expr ::=
property_expr
| multi_clock_sequence
| clocking_event multi_clock_property_expr
| ( multi_clock_property_expr )
| not
multi_clock_property_expr
| multi_clock_property_expr or multi_clock_property_expr
| multi_clock_property_expr and multi_clock_property_expr
|
multi_clock_sequence |-> multi_clock_property_expr
|
multi_clock_sequence |=> [ not ] multi_clock_sequence multi_clock_property_expr
| if ( expression ) multi_clock_property_expr [ else multi_clock_property_expr
]
| property_instance
| ( multi_clock_property_expr )
Two cases are
allowed:
1)
Concatenation of two sequences, where each sequence can have a different clock
2) The
antecedent of an implication on one clock, while the consequent is on another
clock
The
multi-clock concatenation operator ## synchronizes between the two clocks.
@(posedge clk0) sig0 ## @(posedge clk1)
sig1
When signal sig0 matches
at clock clk, ## moves the time to the nearest clock tick of clk1 after
the match. At the first clock tick of clk1, it matches sig1. If the
two clocks, clk0 and clk1, are identical, then the above sequence is
equivalent to:
@(posedge clk0) sig0 ##1 sig1
For two
sequences, such as
@(posedge clk0) s0 ## @(posedge clk1)
s1
For every
match of s0 at clock clk0, ## moves the
time to the first clock tick of clk1. From that first tick of clk1, s1 is
matched.
Multi-clock
implication is only allowed with the non-overlapping implication. The semantics
are similar to the sequence concatenation with ##. Whenever
there is a match of the antecedent sequence, time is advancedto the nearest
clock tick of the clock of the consequent sequence. The consequent is then
evaluated for satisfaction.
17.11.1
Multiply-clocked sequences
Multiply-clocked sequences are built by
concatenating singly-clocked subsequences using the multi-clock concatenation
operator ##.
This operator is non-overlapping and synchronizes between the ending
clock tick of the left hand sequence and the strictly subsequent starting clock
tick of the right hand sequence.
For example, consider
@(posedge clk0) sig0 ## @(posedge
clk1) sig1
A match of this sequence starts with a
match of sig0 at posedge clk0. Then ## moves the time
to the nearest strictly subsequent posedge clk1, and the
match of the sequence ends at that point with a match of sig1. If
clk0 and clk1 are not
identical, then the clocking event for the sequence changes after ##. If
clk0 and clk1 are identical,
then the clocking event does not change after ## and the above sequence is equivalent to
@(posedge clk0) sig0 ##1 sig1
When using the multi-clock concatenation
operator ##, both operands are required to admit only
non-empty matches. Thus, if s1, s2 are sequence
expressions with no clocking events, then the multiply-clocked sequence
@(posedge clk1) s1 ## @(posedge
clk2) s2
is legal only if neither s1 nor s2 can match the
empty word. The clocking event posedge clk1 applies throughout the match of s1, while the clocking event posedge clk2 applies throughout the match of s2.
Since the match of s1 is non-empty,
there is an end point of this match at posedge clk1. The ## synchronizes
between this end point and the first occurrence of posedge clk2 strictly
after it. That occurrence of posedge clk2 is the start
point of the match of s2.
The restriction to operands that do not
match the empty word when using ## ensures that
any multiply-clocked sequence has well-defined starting and ending clocking events
and well-defined clock changes. If clk1 and clk2 are not
identical, then the following sequence
@(posedge clk0) sig0 ## @(posedge
clk1) sig1[*0:1]
is illegal because of the possibility of an
empty match of sig1[*0:1], which would make ambiguous whether the
ending clocking event is posedge clk0 or posedge clk1.
Differently-clocked or multiply-clocked
sequence operands cannot be combined with any sequence operators other than the
multi-clock concatenation operator ##. For
example, the following is illegal:
(@(posedge clk1) x ##1 y) intersect (@(posedge clk2) z[*1:$])
17.11.2
Multiply-clocked properties
As in the case of singly-clocked
properties, the result of evaluating a multiply-clocked property is either true
or false. Multiply-clocked properties
can be formed in a number of ways.
Multiply-clocked sequences are themselves
multiply-clocked properties. For
example,
@(posedge clk0) sig0 ## @(posedge
clk1) sig1
is a multiply-clocked property. If a multiply-clocked sequence is evaluated
as a property starting at some point, the evaluation returns true if and only
if there is a match of the multiply-clocked sequence beginning at that point.
The boolean
property operators (not, and, or) can be used freely to combine singly- and
multiply-clocked properties. The
meanings of the boolean property operators are the
usual ones, just as in the case of singly-clocked properties. For example,
(@(posedge clk0) sig0) and (@(posedge clk1) sig1)
is a multiply-clocked property, but it is not
a multiply-clocked sequence. This
property evaluates to true at a point if and only if the two sequences
@(posedge clk0) sig0
and
@(posedge clk1) sig1
both have matches beginning at the point.
The non-overlapping implication operator |=> can be used freely to create a
multiply-clocked property from an antecedent sequence and a consequent property
that are differently- or multiply-clocked.
The meaning of multiply-clocked non-overlapping implication is similar
to that of singly-clocked non-overlapping implication. For example, if s0, s1 are sequence expressions with no clocking
event, then in
@(posedge clk0) s0 |=> @(posedge
clk1) s1
|=> synchronizes between posedge clk0 and posedge clk1. Starting at the point at which the
implication is being evaluated, for each match of s0 clocked by clk0, time is advanced from the end point of the match to the nearest
strictly future occurrence of posedge clk1, and from
that point there must exist a match of s1 clocked by clk1.
The non-overlapping implication operator |=> can synchronize between the ending clock
event of its antecedent and several leading clock events for subproperties of
its consequent. For example, in
@(posedge clk0) s0 |=> (@(posedge
clk1) s1) and (@(posedge clk2) s2)
|=> synchronizes between posedge clk0 and both posedge clk1 and posedge clk2.
Since synchronization between distinct
clocks always requires strict advance of time, the two property building
operators that require special care with multiple clocks are the overlapping
implication |-> and if/if-else.
Since |-> overlaps
the end of its antecedent with the beginning of its consequent, the clock for
the end of the antecedent must be the same as the clock for the beginning of
the consequent. For example, if clk0 and clk1 are not
identical and s0, s1, s2 are sequence expressions with no clocking
events, then
@(posedge clk0) s0 |-> @(posedge
clk1) s1 ## @(posedge clk2) s2
is illegal, but
@(posedge clk0) s0 |-> @(posedge
clk0) s1 ## @(posedge clk2) s2
is legal.
The if/if-else operators overlap the test
of the boolean condition with the beginning of the
then clause property and, if present, the else clause property. Therefore, whenever using if or if-else, the
then and else clause properties must begin on the same clock as the test of the
boolean condition.
For example, if clk0 and clk1 are not identical and s0, s1, s2 are sequence expressions with no clocking events, then
@(posedge clk0) if (b) @(posedge clk0) s1
is legal, but
@(posedge clk0) if (b) @(posedge clk0) s1 else @(posedge clk1) s2
is illegal because the else clause property
begins on a different clock than the if condition.
17.11.3 Clock
flow
Throughout this subsection, c, d
denote clocking event expressions and v,
w, x, y, z denote sequence expressions with no
clocking events.
Clock flow allows the scope of a clocking
event to extend in a natural way through various parts of multiply-clocked
sequences and properties and reduces the number of places at which the same
clocking event must be specified.
Intuitively, clock flow provides that in a
multiply-clocked sequence or property the scope of a clocking event flows
left-to-right across linear operators (e.g., repetition, concatenation,
negation, implication) and distributes to the operands of branching operators
(e.g., conjunction, disjunction, intersection, if-else) until it is replaced by
a new clocking event.
For example,
@(c) x |=> @(c) y ## @(d) z
can be written more simply as
@(c) x |=> y ## @(d) z
because clock c is understood to flow across |=>.
Clock flow eliminates the need to write
clocking events in positions where the clock is not allowed to change. For example,
@(c) x |-> @(c) y ## @(d) z
can be written as
@(c) x |-> y ## @(d) z
to reinforce the restriction that the clock
not change across |->.
Similarly,
@(c) if (b) @(c) w ## @(d) x else @(c) y ## @(d) z
can be written as
@(c) if (b) w ## @(d) x else y ## @(d) z
to reinforce the restriction that the clock
not change from the boolean condition b
to the beginnings of the then and else clause properties.
Clock flow also makes the adjointness
relationships between concatenation and implication clean for multiply-clocked
properties:
@(c) s1 ##1 s2 |=> @(d) s
is equivalent to
@(c) s1 |=> s2 |=> @(d) s
and
@(c) s1 ##0 s2 |=> @(d) s
is equivalent to
@(c) s1 |-> s2 |=> @(d) s
The scope of a clocking event flows into
parenthesized subexpressions and, if the subexpression is a sequence, also
flows left-to-right across the parenthesized subexpression. However, the scope of a clocking event does
not flow out of enclosing parentheses.
For example, in
@(c) w ## (x ## @(d) y) |=> z
w, x, z
are clocked at c and y is clocked at d. Clock c flows across ##, across the parenthesized sub-sequence (y ## @(d) z), and across |=>. Clock c also flows into the parenthesized sub-sequence, but it does not
flow through @(d). Clock d does not flow out of its enclosing
parentheses.
As another example, in
@(c) v |=> (w ## @(d) x) and (y ## z)
v, w, y,
z are clocked at c and x is clocked at d.
Clock c flows across |=>, distributes to both operands of the and (which is a property conjunction due
to the multiple clocking), and flows into each of the parenthesized subexpressions. Within (w ## @(d) x), c
flows across ## but does not flow through @(d).
Clock d does not flow out of
its enclosing parentheses. Within (y ## z), c
flows across ##.
Similarly, the scope of a clocking event
flows into an instance of a defined sequence or property, and, if the instance
is a sequence, also flows left-to-right across the
instance. However, a clocking event in
the definition of a sequence or property does not flow out of an instance of
that sequence or property.
Note that juxtaposing two clocking events
nullifies the first of them:
@(d) @(c) x
is equivalent to
@(c) x
because the flow of clock d is immediately overridden by clock c.
17.11.4 Examples
The following are examples
of multiple-clock specifications:
6) property
with implication, where antecedent and consequent are named multi-clocked
sequences
property mult_p6;
mult_s |=> mult_s;
endproperty
7) property using clock flow and overlapped
implication:
property mult_p7;
@(posedge clk) a ##1 b |-> c ## @(posedge clk1) d;
endproperty
Here, a, b, and c are clocked at posedge clk.
8) property using clock flow and if-else:
property mult_p8;
@(posedge clk) a ##1 b |->
if (c)
(1 |=> @(posedge clk1) d)
else
e ## @(posedge clk2) f ;
endproperty
Here, a, b, c, and e are clocked at posedge clk.
Like ended, matched can be used directly on sequences
that do not have formal arguments.
An example is shown below:
sequence e1(a,b,c);
@(posedge
clk) $rose(ready a) ##1 proc1 b ##1 proc2 c ;
endsequence
sequence e2;
@(posedge
sysclk)
reset ##1
inst ##1 e1(ready,proc1,proc2).matched
[*->1] ##1 branch_back;
endsequence
In this example, source
sequence e1 is evaluated at clock clk, while the destination sequence e2 is evaluated at clock sysclk. In e2,
the end point of the instance e1(ready,proc1,proc2) is tested to occur sometime after the occurrence of inst. Notice that method matched only tests for the end
point of e1(ready,proc1,proc2) and has no bearing on the starting point of e1(ready,proc1,proc2).
Local variables can be passed into an
instance of a defined sequence to which matched is
applied. The same restrictions apply as
in the case of ended. Values of local variables sampled in an
instance of a defined sequence to which matched is applied
will flow out under the same conditions as for ended. See Section 17.8.
As with ended, a sequence
instance to which matched is applied can have multiple matches in a
single cycle of the destination sequence clock. The multiple matches are
treated semantically the same way as matching both disjuncts of an or. In other words, the thread evaluating
the destination sequence will fork to account for such distinct local variable
valuations.
—
assert to specify the property as a checker to ensure that the property holds
for the design
— assume to
specify the property as an assumption for the environment
procedural_assertion_item
::= //
from Annex A.6.10
assert_property_statement
| cover_property_statement
|
immediate_assert_statement
|
assume_property_statement
assert_property_statement::=
assert property ( property_spec ) action_block
| assert
property ( property_instance
) action_block
assume_property_statement::=
assume property ( property_spec )
cover_property_statement::=
cover property ( property_spec ) statement_or_null
| cover
property ( property_instance
) statement_or_null
The assert, assume or cover statements can be referenced by their
optional name. A hierarchical name can be used consistent with the SystemVerilog
naming conventions. When a name is not provided, a tool shall assign a name to
the statement for the purpose of reporting. Assertion control tasks are
described in Section 23.8.
17.12.1 assert statement
The assert
statement is used to enforce a property
as a checker. When the property for
the assert statement is
evaluated to be true, the pass statements of the action block are executed.
Otherwise, the fail statements of the action_block are executed. For
example,
property abc(a,b,c);
disable iff (a==2)
not @clk (b ##1 c);
endproperty
env_prop: assert property (abc(rst,in1,in2)) pass_stat else fail_stat;
When no
action is needed, a null statement (i.e.;) is specified.
If no statement is specified for the else, then $error is used as the statement when the
assertion fails.
The action_block shall not include any
concurrent assert, assume, or cover statement. The action_block,
however, can contain immediate assertion statements.
Note: The pass and fail
statements are executed in the Reactive region. The regions of execution are
explained in the scheduling semantics section, Section 14.
17.12.2 assume statement
The purpose of
the assume statement
is to allow properties to be considered as assumptions for formal analysis as
well as for dynamic simulation tools. When a property is assumed, the tools
constrain the environment so that the property holds.
For formal
analysis, there is no obligation to verify that the assumed properties hold. An
assumed property can be considered as a hypothesis to prove the asserted
properties.
For simulation,
the environment must be constrained such that the properties that are assumed
shall hold. Like an assert property, an assumed property must be checked and
reported if it fails to hold. There is no requirement on the tools to report
successes of the assumed properties.
Additionally,
for random simulation, biasing on the inputs provides a way to make random
choices. An expression can be associated with biasing as shown below
expression dist
{ dist_list } ; //
from Annex A.1.9
The operator dist and the production dist_list is explained in Section 12.4.4.
The biasing
feature is only useful when properties are considered as assumptions to drive
random simulation. When a property with biasing is used in an assertion or
coverage, the dist operator is equivalent to inside operator, and the weight specification is
ignored. For example,
a1:assume
property @(posedge clk) req dist {0:=40, 1:=60} ;
property proto
@(posedge clk) req |-> req[*1:$] ##0 ack;
endproperty
This is
equivalent to:
a1_assertion:assert
property req inside {0, 1} ;
property proto_assertion
@(posedge clk) req |-> req[*1:$] ##0 ack;
endproperty
In the above
example, signal req is specified with distribution in assumption a1, and is
converted to an equivalent assertion a1_assertion.
It should be
noted that the properties that are assumed must hold in the same way with or
without biasing. When using an assume statement for random simulation, the
biasing simply provides a means to select values of free variables, according
to the specified weights, when there is a choice of selection at a particular
time.
Consider an
example specifying a simple synchronous request - acknowledge protocol, where
variable req can be
raised at any time and must stay asserted until ack is asserted. In the next clock cycle both req and ack must be
deasserted.
Properties
governing req are:
property pr1;
@(posedge clk) !reset_n |-> !req; //when reset_n is asserted
(0),keep req 0
endproperty
property pr2;
@(posedge clk) ack |=> !req; // one cycle
after ack, req must be deasserted
endproperty
property pr3;
@(posedge clk) req |-> req[*1:$] ##0 ack; //
hold req asserted until
// and including ack asserted
endproperty
Properties
governing ack are:
property pa1;
@(posedge clk) !reset_n || !req |-> !ack;
endproperty
property pa2;
@(posedge clk) ack |=> !ack;
endproperty
When verifying the
behavior of a protocol controller which has to respond to requests on req, assertions assert_req1 and assert_req2 should
be proven while assuming that statements a1, assume_ack1, assume_ack2 and assume_ack3 hold at all times.
a1:assume
property @(posedge clk) req dist {0:=40, 1:=60} ;
assume_ack1:assume
property (pr1);
assume_ack2:assume
property (pr2);
assume_ack3:assume
property (pr3);
assert_req1:assert
property (pa1)
else $display("\n ack asserted while req is still
deassrted");
assert_req2:assert
property (pa2)
else $display("\n ack is extended over more than one cycle");
Note that assume
does not provide an action block, as the actions for an assumption serve no
purpose.
17.12.3 cover statement
To monitor
sequences and other behavioral aspects of the design for coverage, the same
syntax is used with the cover statement. The tools can gather
information about the evaluation and report the results at the end of
simulation. When the property for the cover statement is successful, the pass statements
can specify a coverage function, such as monitoring all paths for a sequence. The pass statement shall not include any
concurrent assert, assume or cover statement.
The assert or cover statements
can be referenced by their optional name. A hierarchical name can be used
consistent with the SystemVerilog naming conventions. When a name is not
provided, a tool shall assign a name to the statement for the purpose of
reporting.
Assertion
control tasks are described in Section 23.8.
Coverage
results are divided into two: coverage for properties, coverage for sequences.
For sequence
coverage, the statement appears as:
cover property ( sequence_spec )
statement_or_null
The identifier
of a particular attempt is called attemptId, and the clock tick of the
occurrence of the match is called clock step.
The results of
coverage statement for a property shall contain:
— Number of times attempted
— Number of times succeeded
— Number of times failed
— Number of times succeeded because of
vacuity
— Each attempt with an attemptID and
time
— Each success/failure with an attemptID and
time
In addition, statement_or_null
is executed every time a property succeeds.
Vacuity rules
are applied only when implication operator is used. A property succeeds non-vacuously
only if the consequent of the implication contributes to the success.
Results of
coverage for a sequence shall include:
— Number of times attempted
— Number of times matched (each attempt can
generate multiple matches)
— Each attempt with attemptId and time
— Each match with clock step, attemptID, and
time
In addition, statement_or_null
gets executed for every match. If there are multiple matches at the same
time, the statement gets executed multiple times, one for each match.
—
clocking domain block,
for example:
For a multi-clocked
assertion, the clocks are explicitly specified. No default clock or inferred clock
is used. In addition, multi-clocked properties are not allowed to be defined
within a clocking domain block.
Sequences and properties
specified in clocking domains blocks resolve the clock by the following rules:
1) Event control of the
clocking domain block
specifies the clock.
2) No explicit event
control is allowed in any property or sequence declaration.
3) If a named sequence that
is defined outside the clocking domain block is used, its clock, if specified, must be
identical to the clocking domain’s block’s clock.
— default clock can be
specified using default clocking domain block
17.13.1 Clock resolution in multiply-clocked
properties
Throughout this subsection, s, s1, s2 denote sequence expressions without
clocking events; p, p1, p2 denote property expressions without
clocking events; m, m1, m2 denote multiply-clocked sequences, q, q1, q2 denote multiply-clocked property
expressions; and c, c1, c2 denote non-identical clocking event
expressions.
Due to clock flow, juxtaposition of two
clocks nullifies the first. This and the
nesting of clocking events within other property building operators mean that
there are subtleties in the general interpretation of the restrictions about
where the clock can change in multiply-clocked properties. For example,
@(c) s |-> @(c) (p and @(c1) p1)
appears legal because the antecedent is clocked by
c and the consequent begins
syntactically with the clocking event @(c). However, the consequent sequence is
equivalent to
(@(c) p) and (@(c1) p1)
and |-> cannot
synchronize between clock c from the
antecedent and clock c1
from the second conjunct of the consequent.
Similarly,
@(c) s |-> @(c1) (@(c) p)
appears illegal due to the apparent clock change
from c to c1 across |->. However, it is legal, although arguably
misleading in style, because the consequent property is equivalent to @(c) p.
This subsection gives a more precise
treatment of the restrictions on multiply-clocked use of |-> and if/if-else than the intuitive
discussion in Section 17.11. The present
treatment depends on the notion of the set of semantic leading clocks for a
multiply-clocked sequence or property.
Some sequences and properties have no
explicit leading clock event. Their
initial clocking event is inherited from an outer clocking event according to
the flow of clocking event scope. In
this case, the semantic leading
clock is said to be inherited. For example, in
the property
@(c) s |=> p and @(c1) p1
the semantic leading clock of the subproperty p is inherited
since the intial clock of p is the
clock that flows across |=>.
A multiply-clocked sequence has a unique
semantic leading clock, defined inductively as follows.
·
The
semantic leading clock of s is inherited.
·
The
semantic leading clock of @(c) s is c.
·
If inherited is the semantic leading clock
of m, then the semantic leading clock
of @(c) m
is c.
Otherwise, the semantic leading clock of @(c) m is equal to the semantic leading clock
of m.
·
The
semantic leading clock of (m) is equal to the
semantic leading clock of m.
·
The
semantic leading clock of m1
## m2
is equal to the semantic leading clock of m1.
The set of semantic leading clocks of a
multiply-clocked property is defined inductively as follows.
·
The
set of semantic leading clocks of m
is {c}, where c
is the unique semantic leading clock of m.
·
The
set of semantic leading clocks of p
is {inherited}.
·
If inherited is an element of the set of
semantic leading clocks of q, then
the set of semantic leading clocks of @(c) q
is obtained from the set of semantic leading clocks of q by replacing inherited by c. Otherwise, the set of semantic leading clocks
of @(c) q
is equal to the set of semantic leading clocks of q.
·
The
set of semantic leading clocks of (q) is equal to the
set of semantic leading clocks of q.
·
The
set of semantic leading clocks of not q is equal to the set of semantic leading clocks of q.
·
The
set of semantic leading clocks of q1
and q2 is the union of the set of
semantic leading clocks of q1 with the set of
semantic leading clocks of q2.
·
The
set of semantic leading clocks of q1
or q2 is the union of the set of
semantic leading clocks of q1
with the set of semantic leading clocks of q2.
·
The
set of semantic leading clocks of m |-> p is equal to the set of semantic leading
clocks of m.
·
The
set of semantic leading clocks of m |=> p is equal to the set of semantic leading
clocks of m.
·
The
set of semantic leading clocks of if (b) q is {inherited}.
·
The
set of semantic leading clocks of if (b) q1 else q2 is {inherited}.
·
The set
of semantic leading clocks of a property instance is equal to the set of
semantic leading clocks of the multiply-clocked property obtained from the body
of its definition by substituting in actual arguments.
For example, the multiply-clocked sequence
@(c1) s1 ## @(c2) s2
has c1
as its unique semantic leading clock, while the multiply-clocked property
not (p1 and (@(c2) p2)
has {inherited,
c2} as its set of semantic
leading clocks.
In the presence of an incoming outer clock,
the inherited semantic leading clock
is always understood to refer to the incoming outer clock. On the other hand, if a property has only
explicit semantic leading clocks, then the incoming outer clock has no effect
on the clocking of the property since the explicit clock events replace the
incoming outer clock. Therefore, the
clocking of a property q in the
presence of incoming outer clock c is
equivalent to the clocking of the property @(c) q.
The rules for using multiply-clocked
overlapping implication and if/if-else in the presence of an incoming outer
clock can now be stated more precisely.
1.
Multiply-clocked
overlapping implication.
Let c
be the incoming outer clock. Then the
clocking of m |-> q is equivalent to the clocking of @(c) m |-> q
In the presence of the incoming outer
clock, m has a well-defined ending
clock, and there is a well-defined clock that flows across |->.
The multiply-clocked overlapped implication m |-> q is legal for incoming clock c
if and only if the following two conditions are met:
a.
Every
explicit semantic leading clock of q
is identical to the ending clock of m.
b. If inherited
is a semantic leading clock of q,
then the ending clock of m is equal
to the clock that flows across |->.
For example
@(c) s |-> p1 or @(c2) p2
is not legal because the ending clock of the
antecedent is c, while the consequent
has c2 as an explicit
semantic leading clock.
Also,
@(c) s ## (@(c1) s1) |-> p
is not legal because the set of semantic
leading clocks of p is {inherited}, the ending clock of the
antecedent is c1, and the
clock that flows across |-> and is
inherited by p is c.
On the other
hand,
@(c) s |-> p1 or @(c) p2
and
@(c) s ## @(c1) s1 |-> p1 or @(c1) p2
are both
legal.
1.
Multiply-clocked
if/if-else
Let c
be the incoming outer clock. Then the
clocking of if (b) q1 [ else q2
] is equivalent to the clocking of
@(c) if (b) q1 [ else q2 ]
The boolean condition b is clocked by c, so the
multiply-clocked if/if-else if (b) q1 [
else q2 ] is legal for incoming
clock c if and only if the following
condition is met:
o
Every
explicit semantic leading clock of q1
[ or q2
] is identical to c.
For example,
@(c) if (b) p1 else @(c) p2
is legal, but
@(c) if (b) @(c) (p1 and @(c2) p2)
is not.
statement_item ::=
...
| expect ( property_spec )
[ action_block ]
| expect ( property_instance
) [ action_block ]
expect_property_statement ::=
expect ( property_spec ) action_block