Subject: [sv-ec] Re: [sv-ac] Constraint implication, sequence implication, and transitions
From: David W. Smith (David.Smith@synopsys.com)
Date: Sun Nov 16 2003 - 10:50:23 PST
Hi Jay,
Just to make the argument that we discussed at the Face-to-Face meeting
available to all in SV-AC and SV-EC I have sent the following.
1. I agree that consistency is useful here.
2. The most common symbols I can find, doing searches of font standards,
languages, and the web, are the following operators for implication:
=>, -->, ->, >>, subset notation. The most popular (HTML-4.0, Mathworld,
Algol-60, Python, etc), by far, is =>. Please see the attached word document
for the references.
3. The -> used for transition has some relation to the event trigger
operator and is more natural for users.
4. It seems, that for the greatest consistency that the operators used, SVA
could be changed so that overlapping and non-overlapping semantics would be
indicated in a common way with the already common usage for implication.
This seems to make more sense since no one that I have presented the |=> or
|-> operators to, without explanation, interpreted the overlap vs
non-overlap as defined in SVA. They immediately assumed the opposite (as
proposed below).
So, to present your table using this argument:
=> overlapping constraint implication
|=> overlapping sequence implication
|-> non-overlapping sequence implication
-> non-overlapping transition
##0 overlapping cycle delay
##1 non-overlapping cycle delay
Regards
David
----- Original Message -----
From: "Jay Lawrence" <lawrence@cadence.com>
To: <sv-ec@eda.org>; <sv-ac@eda.org>
Sent: Friday, November 07, 2003 2:50 PM
Subject: [sv-ac] Constraint implication, sequence implication, and
transitions
>
> 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 : Sun Nov 16 2003 - 10:53:30 PST