Subject: RE: [sv-ec] Re: [sv-ac] Constraint implication, sequence implicat ion, and transitions
From: Warmke, Doug (doug_warmke@mentorg.com)
Date: Mon Nov 17 2003 - 13:26:00 PST
David,
Your #1 point (and Jay's) is very good: Consistency is important.
I think we should go for it right now in SV 3.1a.
I understand that you searched the Internet to find the most
common mathematical notations used for the concepts under discussion.
However, PSL is the major comparable benchmark in our own industry.
I believe we should try to conform to the most common notation used
in our own industry rather than the most common notation world-wide.
Now, why the PSL team opted to use the less common notation is
another question... But IMO it is fait accompli at this time,
and we should go with the flow.
Thanks and regards,
Doug
> -----Original Message-----
> From: owner-sv-ec@eda.org [mailto:owner-sv-ec@eda.org] On
> Behalf Of David W. Smith
> Sent: Sunday, November 16, 2003 10:50 AM
> To: Jay Lawrence; sv-ec@eda.org; sv-ac@eda.org
> Subject: [sv-ec] Re: [sv-ac] Constraint implication, sequence
> implication, and transitions
>
>
> 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 : Mon Nov 17 2003 - 13:42:48 PST