Subject: [sv-ec] Constraint implication, sequence implication, and transitions
From: Jay Lawrence (lawrence@cadence.com)
Date: Fri Nov 07 2003 - 14:50:50 PST
Sv-ec and sv-ac members:
When reviewing the "functional coverage" proposal in the sv-ec last
week, the use of the operator '->' for indicating a state transition was
discussed. During this discussion, I took the position that state
transition (i.e. 0 -> 1) was equivalent to the '##' operator in
sequences. It is essentially a "next()" operator and therefore we
should reuse the '##' operator for consistency with sequences in
properties.
This motion did not succeed to get the change adopted so I took an
action item to document my concerns. To fulfill that AI, I've looked at
all of the variations of implication and sequencing in SV3.1a that I can
find. I'm sending the analysis to multiple groups because there are
slightly different forms of implication in each committee that I
believe should be resolved.
12.4.5 [ Constraint ] Implication
---------------------------------
In this section the "=>" operator is introduced "to declare an
expression that implies a constraint".
The syntax is:
constraint_expression ::=
...
| expression => constraint_set
"This states that if the expression is true, then random numbers
generated are constrained by the constraint (or constraint block)."
Examples include (parenthesis added for clarity):
(mode == small) => (len < 10);
or
(mode == large) => (len > 100);
Note that this is an "overlapping operator" to borrow a definition from
sequences. If the expression holds in the current cycle, then the
constraint must be satisfied in this cycle.
17.6 Declaring Sequences
------------------------
This section declares sequences for use in assertions. It is mentioned
here because the coverage transition syntax utilizes a subset of the
sequence syntax.
The basic specification of a sequence is a series of boolean expressions
separated by a "cycle_delay_range" which is the "##" operator.
For example:
sequence s1;
@(posedge clk) (mode == large) ##0 (len < 10);
endsequence
The constant following the ## controls whether this is "overlapping" or
"non-overlapping". In its simplest form the number is the cycle in which
it should occur (ranges and various other forms are also supported). A
value of zero indicates overlap of the left and right hand sides. A
value of 1 indicates that it should happen in the "next" cycle.
17.7.11 [ Sequence ] Implication
--------------------------------
This section introduces the two operators "|->" and "|=>" for
implications between sequences at the property level.
property_expr ::=
...
| sequence_expr |-> [ not ] sequence_expr
| sequence_expr |=> [ not ] sequence_expr
The "|->" operator is an "overlapping" operator. When the last element
in the sequence on the left hand side is true, then the first element
on the right hand side must hold in the SAME cycle.
The "|=>" operator is a "non-overlapping" operator. When the last
element in the sequence on the left hand side is true, then the first
element on the right hand side must hold in the NEXT cycle.
Therefore:
sequence_expr |=> sequence_expr
is equivalent to:
sequence_expr ##1 true |-> sequence_expr
An example of a property that would check that the above constraint
implication was properly generated would be:
property small_mode_check;
@(posedge clk)
(mode == small) |-> (len < 10);
endproperty
20.4.1 Specifying bins for transitions
--------------------------------------
In the coverage proposal a coverage point bin can be defined as a
transition between 2 values (or sets of values). I've given a subset of
the grammar here that just includes the simplest form of the
transition. The issues w.r.t. overlap with implication and sequences
are unaffected by this simplification.
The simplified grammar is:
trans_list ::= trans_set { , trans_set }
trans_set ::= trans_range_list -> trans_range_list
trans_range_list ::=
trans_item
| ...
trans_item ::= { range_list } | value_range
So an example bin to hold a transition coverage point would be:
covergroup mgroup @(posedge clk);
coverpoint mode { // mode is the variable being covered
bins sl = (small -> large); // mode goes from small to
large
bins ls = (large -> small); // mode goes from large to
small
}
endgroup
The behavior of this is that (small -> large) is true when the mode
variable equals small on one posedge clk and equals large on the "next"
posedge clock. As such the "->" operator is a "non-overlapping"
operator.
---------------------
Summary of operators:
---------------------
=> overlapping constraint implication
|-> overlapping sequence implication
|=> non-overlapping sequence implication
-> non-overlapping transition
##0 overlapping cycle delay
##1 non-overlapping cycle delay
--------------
Analysis
--------------
My original recommendation in the sv-ec meeting was that "->" be
replaced by ##1 because it really means "In the next cycle the next
value should be true.
After this exercise I think this is not the correct solution but some
unification should happen between sv-ec and sv-ac on this issue. A
consistency between constrain implication, sequence implication, and
transition should be adopted across the language.
Alternative 1:
--------------
Here we get down to 2 operations, one for overlapping one for
non-overlapping.
|-> overlapping implication (constraints and sequences)
|=> transition and non-overlapping implication
Alternative 2:
--------------
If for some reason the same operator should not be used for constraints
and sequences the operators should be respecified as (* indicates
changed item):
-> overlapping constraint implication*
|-> overlapping sequence implication
|=> non-overlapping sequence implication
=> non-overlapping transition*
This would follow the convention that "-" is always overlapping and "="
is always non-overlapping. Note that this would also bring better
alignment between PSL and SVA where PSL uses -> as boolean implication
(which is analagous to constraint implication in SV).
---------
Examples
---------
Taking a few examples for above, and putting them side to side to make
the issue more explicit.
Without any changes:
--------------------
The constraint to generate mode and len would be:
constraint c { (mode == small) => (len < 10); }
A sequence to check it would be:
sequence s1;
@(posedge clk) (mode == large) ##0 (len < 10);
endsequence
A property to check it would be:
property small_mode_check;
@(posedge clk)
(mode == small) |-> (len < 10);
endproperty
A coverage group to record it's occurrence would be:
covergroup mgroup @(posedge clk);
coverpoint mode {
bins sl = (small -> large);
bins ls = (large -> small);
}
endgroup
Note we have used all of =>, ##0, |->, and ->
With the changes (Alternative 2):
---------------------------------
The constraint to generate mode and len would be:
constraint c { (mode == small) -> (len < 10); }
A sequence to check it would be:
sequence s1;
@(posedge clk) (mode == large) ##0 (len < 10);
endsequence
A property to check it would be:
property small_mode_check;
@(posedge clk)
(mode == small) |-> (len < 10);
endproperty
A coverage group to record it's occurrence would be:
covergroup mgroup @(posedge clk);
coverpoint mode {
bins sl = (small => large);
bins ls = (large => small);
}
endgroup
The overlapping constraint and property use '-' forms, the coverage
tranition uses "=>".
Jay
===================================
Jay Lawrence
Senior Architect
Functional Verification
Cadence Design Systems, Inc.
(978) 262-6294
lawrence@cadence.com
===================================
This archive was generated by hypermail 2b28 : Fri Nov 07 2003 - 14:53:25 PST