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_or_dist [ boolean_abbrev ]
| (expression_or_dist {, variable_assignment sequence_match_item} ) [ boolean_abbrev ]
| sequence_instance [ sequence_abbrev ]
| ( sequence_expr {, variable_assignment sequence_match_item
} ) [ 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
sequence_match_item ::=
variable_assignment
| subroutine_call
…
| expression_or_dist [ boolean_abbrev ]
| (expression_or_dist {, variable_assignment sequence_match_item} ) [ boolean_abbrev ]
| sequence_instance [ sequence_abbrev ]
| ( sequence_expr {, variable_assignment sequence_match_item
} ) [ sequence_abbrev ]
…
— expression
[*n:m], where n is the
minimum, m is the maximum [*m:n], where m is the minimum, n is the maximum, and m >= 0, m<= n or
n is $
This is equivalent to:
a ##1
((!b [*0:$] ##1 b)) [*min:max])
##1 c
This is equivalent to:
a ##1 ((!b [*0:$] ##1 b)) [*min:max]) ##1
!b[*0:$] ##1 c
The following example is an
expression with the and
and operator,
where the two operands are single sequence evaluations. The operation is illustrated in Figure 17-4.
The operation as
illustrated in Figure 17-4 shows the evaluation attempt at clock tick 8. Here, The
the two operand
sequences are (te1 ##2 te2) and
(te3 ##2 te4 ##2 te5). The first
operand sequence requires that first te1 evaluates to true followed by te2 two clock ticks later. The second sequence requires
that first te3 evaluates to true followed
by te4 two clock ticks later,
followed by te5 two clock ticks later. Figure 17-4 shows the evaluation attempt at clock tick 8.
Add a dashed box around the two green arrows showing matches on the last grid line
Add a dashed box around the five green arrows showing matches on the last grid line
If signal burst_mode were to be
maintained low until at least clock tick 10,
the expression would result in a match as shown in Figure 17-12.
!trdy[*7] within
(($fell irdy) ##1 !irdy[*8])
EDITOR’S NOTE: The use of “iff” in a non-keyword context is not defined in the LRM
(though annex H uses it extensively). I changed “iff”
to “if and only if” for the context above.
specifies looking for the rising edge of frame within two clock ticks in the future. After frame toggles high, irdy must also toggle high after one clock tick. This is illustrated
in Figure 17-14 for the evaluation attempt at clock
tick 6. ‘data_end_exp
is acknowledged at clock tick 6. Next, frame toggles high at clock tick 7. Since this falls within
the timing constraint imposed by [1:2], it satisfies the sequence and continues to monitor evaluate
further. At clock tick 8, irdy is evaluated. Signal irdy transitions to high at clock tick 8, satisfying matching
the sequence specification completely for the attempt that began at clock tick
6.
…
| (expression_or_dist {, variable_assignment sequence_match_item} ) [ boolean_abbrev ]
| ( sequence_expr {, variable_assignment sequence_match_item
} ) [ sequence_abbrev ]
…
1) When valid_in is true, x is assigned to pipe_in.
Property e is true if five cycles later, x pipe_out1 is
equal to (x+1). Property e is false if pipe_out1
is not equal to (x+1).
sequence
data_check;
int
x;
a ##1 !a, x = data_in ##1 !b*[0:$] b[*0:$] ##1 b && (data_out
== x);
endsequence
property
data_check_p
int
x;
a ##1 !a, x = data_in |=> !b*[0:$]
b[*0:$] ##1 b && (data_out
== x);
endproperty
sequence
sub_seq1;
int
v1;
a ##1 !a, v1 = data_in ##1 !b*[0:$] b[*0:$] ##1 b && (data_out
== v1);
endsequence
sequence
sub_seq2(lv);
a ##1
!a, lv = data_in ##1 !b*[0:$] b[*0:$]
##1 b && (data_out == lv);
endsequence
sequence
sub_seq3(lv);
int
lv; // illegal since lv is a formal argument
a ##1 !a, lv = data_in ##1 !b*[0:$] b[*0:$]
##1 b && (data_out == lv);
endsequence
17.9 Calling subroutines on match of a sequence
Tasks, task methods, void functions, void function methods, and
system tasks can be called at the end of successful match of a sequence. The subroutine calls, like local variable
assignments, appear in the comma-separated list that follows the sequence. The subroutine calls are said to be attached to the sequence. The sequence and the list that follows are
enclosed in parentheses.
sequence_expr ::= // from Annex A.2.10
...
| ( expression_or_dist { , sequence_match_item } ) [ boolean_abbrev
]
| ( sequence_expr { , sequence_match_item } ) [ sequence_abbrev
]
...
sequence_match_item ::=
variable_assignment
| subroutine_call
Syntax 17-14 – subroutine call in sequence syntax (excerpt from
Annex A)
For example,
sequence s1;
logic v, w;
(a, v = e) ##1
(b[*->1], w = f,
$display("b after a with v = %h, w = %h\n", v, w));
endsequence
defines a sequence s1 that matches at
the first occurrence of b strictly after an occurrence of a. At the match, the system task $display is
executed to write a message that announces the match and shows the values
assigned to the local variables v and w.
All subroutine calls attached to a sequence are executed at every
successful match of the sequence. For
each successful match, the attached calls are executed in the order they appear
in the list. The subroutines are
scheduled in the Reactive region, like an action block.
Each argument of a subroutine call attached to a sequence must
either be passed by value as an input or be passed by reference (either ref or const ref; see Section 10.4.2). Actual argument expressions that are passed
by value use sampled values of the underlying variables and are consistent with
the variable values used to evaluate the sequence match.
Local variables can be passed into subroutine calls attached to a
sequence. Any local variable that flows
out of the sequence or that is assigned in the list following the sequence, but
before the subroutine call, can be used in an actual argument expression for
the call. If a local variable appears in
an actual argument expression, then that argument must be passed by value.
EDITOR’S NOTE: In many places in this and subsequent
subsections of Section 17, the draft 3 change orders called for the keyword
pair if-else, with a dash separating them.
The convention used elsewhere in the LRM for keyword pairs is to separate them
with an ellipsis, such as begin...end and if...else. I
followed the LRM convention, and changed all occurrences “if-else” to “if...else“. Was
this the correct thing to do for each occurrence, or was the pair “if-else”
sometimes being used as a non-keyword term?
The if/if...else operators overlap the test of the boolean condition with the beginning of the then if clause property
and, if present, the else clause property.
Therefore, whenever using if
or
if...else, the then if and else 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
EDITOR’S NOTE: There seems to be
a problem with the wording in the previous paragraph. What is meant by “...the
then and else clause...”? Is “then” a new keyword? If so, I
did not see it in any BNF changes, or as an addition to Annex A. If the
“then” in “then and else clause” has a meaning, it needs to be defined.
Throughout this subsection,
c, d c,
d denote
clocking event expressions and v, w, x, y, z 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,
@(cc) xx |=>
@(cc) yy
## @(dd)
zz
can be written more simply as
@(cc) xx |=>
yy ## @(dd) zz
because clock cc 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,
@(cc) xx |->
@(cc) yy
## @(dd)
zz
can be written as
@(cc) xx |->
yy ## @(dd) zz
to reinforce the restriction that the clock not change
across |->. Similarly,
@(cc) if (bb) @(cc) ww ## @(dd) xx else
@(cc) yy ## @(dd) zz
can be written as
@(cc) if (bb) ww
## @(dd)
xx else yy ## @(dd) zz
to reinforce the restriction that the
clock not change from the boolean condition bb to the beginnings of the then if and else else clause
properties.
EDITOR’S NOTE: There seems to be
a problem with the wording in the previous paragraph. What is meant by “...the
then and else clause...”? Is “then” a new keyword? If so, I
did not see it in any BNF changes, or as an addition to Annex A. If the
“then” in “then and else clause” has a meaning, it needs to be defined.
Clock flow also makes the adjointness relationships between concatenation and
implication clean for multiply-clocked properties:
@(cc) s1x ##1 s2y |=> @(dd) sz
is equivalent to
@(cc) s1x |=>
s2y |=> @(dd) sz
and
@(cc) s1x ##0 s2y |=> @(dd) sz
is equivalent to
@(cc) s1x |->
s2y |=> @(dd) sz
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
@(cc) ww
## (xx ## @(dd) yy) |=> zz
w, x, z w, x, z are clocked at cc and yy is clocked
at dd. Clock cc flows
across ##, across the parenthesized sub-sequence (yy ## @(dd) zz),
and across |=>. Clock cc also flows into the parenthesized sub-sequence, but it
does not flow through @(dd). Clock dd does not
flow out of its enclosing parentheses.
As another example, in
@(cc) vv |=>
(ww ## @(dd) xx) and
(yy
## zz)
v, w, y, z v, w, y, z are clocked at cc and xx is clocked
at dd. Clock cc 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 (ww
## @(dd)
xx), cc flows
across ## but does not flow through @(dd).
Clock dd does not flow out of its enclosing parentheses. Within
(yy
## zz), cc 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:
@(dd) @(cc) xx
is equivalent to
@(cc) xx
because the flow of clock dd is immediately
overridden by clock cc.
To detect the end point of
a sequence when the clock of the source sequence is different than the desalination destination
sequence, method matched on
the source sequence is used. The end point of a sequence is reached whenever
there is a match on its expression. The occurrence of the end point can be
tested in any sequence expression by using the method ended when the clocks of the source and destination
sequences are the same, while method matched is used when the clocks are different.
module top(input
bit clk);
logic a,b,c;
sequence seq3;
@(posedge clk) b ##1 c;
endsequence
c1: cover
property cover property (seq3);
...
endmodule
property
rule;
a ##1 b
##1 c;
endproperty
always
@(posedge
clk) begin begin
<statements>;
assert property assert property (rule);
end
property
r3;
@(posedge
sclk mclk)(q != d);
endproperty
always
@(posedge
mclk) begin
if
(a) begin
q <= d1;
r3_p: assert property (r2 r3);
end
end
The above example is
equivalent to:
property
r3;
@(posedge
sclk mclk)a |-> (q != d);
endproperty
r3_p: assert property (r3);
always
@(posedge mclk) begin
if
(a) begin
q <= d1;
end
end
property
r4;
@(posedge
sclk mclk)(q != d);
endproperty
property
r4;
@(posedge
sclk mclk)(a==1) |-> (q !=
d);
endproperty
—
default clock,
for example:
default
clocking master_clk @(posedge
clk);
property p4; (a ##2 b); endproperty
assert property (p4);
These example sequences are
used in Table 17-3 to explain the clock resolution rules for a sequence
definition. The clock of any sequence when explicitly specified is indicated by
X. The absence of a clock Otherise, it is indicated by a dash.
Throughout this subsection,
s, s1, s2 s,
s1, s2 denote sequence expressions without clocking events; p, p1, p2 p,
p1, p2 denote property expressions without clocking events; m, m1, m2 m,
m1, m2 denote multiply-clocked sequences, q, q1, q2 q,
q1, q2 denote multiply-clocked property expressions; and c, c1, c2 c,
c1, c2 denote non-identical clocking event expressions.
EDITOR’S NOTE:
The change order for this new section used italics for signal names that appear
in the code examples, and some the signal names had subscripts. The convention
used elsewhere in this LRM is to use Courier font for signal names. I used the
LRM convention of Courier font. Since actual code cannot have subscripts, I did
not use the subscripts that were in the change order.
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,
@(cc) ss |-> @(cc) (pp and
@(c1c1) p1p1)
appears legal because the antecedent is clocked by cc and the
consequent begins syntactically with the clocking event @(c1c1).
However, the consequent sequence is equivalent to
(@(cc) pp) and
(@(c1c1) p1p1)
and |-> cannot synchronize between clock cc from the
antecedent and clock c1c1 from the second conjunct of the consequent. Similarly,
(@(cc) ss
|-> (@(c1c1) (@(cc) pp)
appears illegal due to the apparent clock change from cc to c1c1 across
|->. However, it is legal, although arguably misleading in style, because
the consequent property is equivalent to @(cc) pp.
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
@(cc) ss |=> pp and @( c1c1) p1p1
the semantic leading clock of the subproperty
pp is inherited inherited since the
initial clock of pp 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 ss is inherited inherited.
—
The semantic
leading clock of @(cc) ss is cc.
—
If inherited is
the semantic leading clock of mm, then the semantic leading clock of @(cc) mm is cc. Otherwise, the semantic leading clock of @(cc) mm is equal to the semantic leading clock of mm.
—
The semantic
leading clock of (mm) is equal to the semantic leading clock of mm.
—
The semantic
leading clock of m1m1 ## m2m2 is
equal to the semantic leading clock of m1m1.
The set of semantic leading
clocks of a multiply-clocked property is defined inductively as follows.
—
The set of
semantic leading clocks of mm is {cc}, where cc is the unique semantic leading clock of mm.
—
The set of
semantic leading clocks of pp is {inherited}.
—
If inherited is
an element of the set of semantic leading clocks of qq, then the set of
semantic leading clocks of @(cc) qq
is obtained from the set of semantic
leading clocks of qq by replacing inherited inherited
by cc. Otherwise, the set of
semantic leading clocks of @(cc) qq is equal to the set of semantic leading clocks of qq.
—
The set of
semantic leading clocks of (qq) is
equal to the set of semantic leading clocks of qq.
—
The set of
semantic leading clocks of not qq is equal
to the set of semantic leading clocks of qq.
—
The set of
semantic leading clocks of q1q1 and q2q2 is the union of the set of semantic leading clocks of q1q1 with
the set of semantic leading clocks of q2q2.
—
The set of
semantic leading clocks of q1q1 or q2q2 is the union of the set of semantic leading clocks of q1q1 with
the set of semantic leading clocks of q2q2.
—
The set of
semantic leading clocks of mm
|-> pp is equal to the set of semantic leading clocks of mm.
—
The set of
semantic leading clocks of mm
|=> pp is equal to the set of semantic leading clocks of mm.
—
The set of
semantic leading clocks of if (bb) qq
is {inherited}.
—
The set of
semantic leading clocks of if (bb) q1q1
else q2q2 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
@(c1c1) s1s1
## @(c2c2) s2s2
has c1c1 as its unique semantic leading clock, while the
multiply-clocked property
not
(p1p1 and
(@(c2c2) p2p2)
has {inherited, c2c2} 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 qq in the
presence of incoming outer clock cc is equivalent to the clocking of the property @(cc) qq.
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 cc be the
incoming outer clock. Then the clocking of mm
|-> qq
is equivalent to the clocking of @(cc) mm |->
qq
In the presence of the
incoming outer clock, mm has a
well-defined ending clock, and there is a well-defined clock that flows across
|->. The multiply-clocked overlapped implication mm |-> qq is
legal for incoming clock cc if and only if the following two conditions are met:
a) Every explicit semantic
leading clock of qq is identical to the ending clock of mm.
b) If inherited inherited is a
semantic leading clock of qq, then the ending clock of mm is equal
to the clock that flows across |->.
For example
@(cc) ss
|-> p1p1 or
@(c2c2) p2p2
is not legal because the ending clock of the antecedent
is cc, while the consequent
has c2c2 as
an explicit semantic leading clock.
Also,
@(cc) ss
## (@(c1c1) s1s1) |-> pp
is not legal because the set of semantic leading clocks
of pp is {inherited},
the ending clock of the antecedent is c1c1, and the clock that flows across |-> and is
inherited by pp is cc.
On the other hand,
@(cc) ss
|-> p1p1 or
@(cc) p2p2
and
@(cc) ss
## @(c1c1) s1s1 |-> p1p1
or @(c1c1)
p2p2
are both legal.
2) Multiply-clocked if/if...else
Let cc be the
incoming outer clock. Then the clocking of if (bb) q1q1
[ else q2q2 ] is
equivalent to the clocking of
@(cc) if (bb) q1q1
[ else q2q2 ]
The boolean
condition bb is clocked
by cc, so the
multiply-clocked if/if...else if (bb) q1q1
[ else q2q2 ] is
legal for incoming clock cc if and only if the following condition is met:
— Every explicit semantic
leading clock of q1q1 [ or
q2q2 ] is
identical to cc.
For example,
@(cc) if (bb) p1p1
else @(cc) p2p2
is legal, but
@(cc) if (bb) @(cc) (p1p1 and @(c2c2) p2p2)
is not.
interface range (input clk,enable, input int
minval,expr);
property crange_en;
@(posedge clk) enable enable |-> (minval
<= expr);
endproperty
range_chk: assert property (crange_en);
endinteface
bind cr_unit range r1(c_clk,c_en,v_low,(in1&&in2));