Subject: [sv-ec] FW: Email from John Havlicek
From: David W. Smith (David.Smith@synopsys.com)
Date: Sun Nov 16 2003 - 22:40:47 PST
Regards
David
----- Original Message -----
From: <owner-sv-ec@eda.org>
To: <owner-sv-ec@eda.org>
Sent: Sunday, November 16, 2003 11:41 AM
Subject: BOUNCE sv-ec@eda.org: Non-member submission from [John Havlicek
<john.havlicek@motorola.com>]
> >From owner-sv-ec Sun Nov 16 11:40:06 2003
> Received: from motgate3.mot.com (motgate3.mot.com [144.189.100.103])
> by server.eda.org (8.12.0.Beta7/8.12.0.Beta7) with ESMTP id
hAGJe48h004554;
> Sun, 16 Nov 2003 11:40:05 -0800 (PST)
> Received: from az33exr01.mot.com (az33exr01.mot.com [10.64.251.231])
> by motgate3.mot.com (Motorola/Motgate3) with ESMTP id hAGJdxEJ003071;
> Sun, 16 Nov 2003 12:39:59 -0700 (MST)
> Received: from adttx.sps.mot.com (adttx.sps.mot.com [163.12.136.93])
> by az33exr01.mot.com (Motorola/az33exr01) with ESMTP id hAGJcrDZ018829;
> Sun, 16 Nov 2003 13:38:55 -0600
> Received: from tamale.sps.mot.com (tamale [163.12.136.135])
> by adttx.sps.mot.com (8.11.7+Sun/8.10.2) with ESMTP id hAGJdwr18471;
> Sun, 16 Nov 2003 13:39:58 -0600 (CST)
> Received: (from havlicek@localhost)
> by tamale.sps.mot.com (8.11.7+Sun/8.10.2) id hAGJdvB04440;
> Sun, 16 Nov 2003 13:39:57 -0600 (CST)
> Date: Sun, 16 Nov 2003 13:39:57 -0600 (CST)
> Message-Id: <200311161939.hAGJdvB04440@tamale.sps.mot.com>
> To: David.Smith@synopsys.com
> CC: lawrence@cadence.com, sv-ec@server.eda.org, sv-ac@server.eda.org,
> vfv@server.eda.org
> In-reply-to: <00d801c3ac72$7e42ebb0$6b01a8c0@torres>
> (David.Smith@synopsys.com)
> Subject: Re: [sv-ac] Constraint implication, sequence implication, and
transitions
> From: John Havlicek <john.havlicek@motorola.com>
> Reply-to: john.havlicek@motorola.com
> References:
<0D3972F302D58440BD35BF14DC48AF5601AA3CFF@exmbx01chel.cadence.com>
<00d801c3ac72$7e42ebb0$6b01a8c0@torres>
>
> David:
>
> I think that "->" is a commonly used notation for logical
> implication in mathematical logic.
>
> Your proposal does not consider the alignment of SVA and PSL.
>
> The operators "|->" and "|=>" were inherited from PSL, and your
> proposal will exactly reverse the meanings from what they are
> in PSL.
>
> I think that if it is desired to change the meanings in the way
> that you describe, then the case for this should be made to the
> FVTC and the change should be approved there first.
>
> Best regards,
>
> John H.
>
> >
> > This is a multi-part message in MIME format.
> >
> > ------=_NextPart_000_00D5_01C3AC2F.6FA6F940
> > Content-Type: text/plain;
> > charset="iso-8859-1"
> > Content-Transfer-Encoding: 7bit
> >
> > 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 - 22:42:49 PST