Subject: [sv-ac] Re: [Fwd: Re: Supporting general case of assertion functions and .ended/matched]
From: Surrendra Dudani (Surrendra.Dudani@synopsys.com)
Date: Fri Nov 14 2003 - 08:25:18 PST
Hi Adam,
events are not allowed in sequences, so .triggered cannot be used in
sequences either. They cannot be used in formal. If .triggered is used in
sequences, its value will be always false, as it gets sampled. If it is not
sampled, then its value will never be deterministic.
On the other hand, .ended only provides the end point of a sequence, and it
can only be used with the same clock of the source and destination sequences.
So, here is my conclusion, If we make .triggered as .ended and remove
.ended, then we will have two different definitions of it, one in the use
of assertions, and one outside. It will also create confusion, as one might
think that events are allowed in assertions.
Similarly, if we allow .ended to be used outside the sequences, it will
again have two definitions for its two usages. The question of .triggered
will still remain, since sequences generate a "virtual" event outside the
assertions in the reactive region. So, why .triggered wouldn't be allowed
on them?
With John's extension of allowing local variables in and out of .ended, it
will create additional complexity in its meaning outside the sequences.
Those are my reasons to keep the two (.ended and .triggered) separate, and
clean, as they are defined.
Surrendra
At 09:48 AM 11/14/2003 -0600, you wrote:
>HI Surrendra;
>
>Forwarding the original mail and my responses to sv-ac for their comments...
>
>You wrote:
>
> >> I would like to see this merged with ".ended" as they appear to be the
> same
> >> idea.
>
>
> >We thought quite a bit about this, but decided to keep the two methods.
> Although their >functionality overlaps "in spirit", merging the two
> caused other problems, such as
> >1) Detecting the end of sequences using @ operator implies that the end
> of sequence >"generates" an event. So triggered seems applicable.
> >2) The use of ended in sequences as well as in the code can cause
> confusion about its >semantics, since ended have a special treatment in
> sequences. Sequences using ended are >automatically ordered to get the
> correct results. Cyclic use of ended is not allowed, >etc.
> >3) Formal semantics for ended can only be partially defined for its use
> in sequences
>
>I believe that here is an excellent case for reuse and simplification of
>sequences.
>There are two contexts being discussed here, event expression context and
>sequence
>context.
>
>I do not believe there is any overlap in these two contexts, thus there
>should be
>no ambiguity. To have two different methods, one and only one for each
>context seems
>so serve no use but confusion.
>
>As currently proposed seq.triggered and seq.ended are both boolean
>expressions.
>Thus aren't these sequences (second_one, third_one) equivalent? If they are
>different, when would one want to use .ended and when would one want to use
>.triggered.
>
>
>sequence first_one
> (a ##1 b ##1 c);
>endsequence
>
>sequence second_one
> first_one.ended ##1 d ##1 e ##1 f);
>
>endsequence
>
>sequence third_one
> (first_one.triggered ##1 d ##1 e ##1 f);
>endsequence.
>
>I thought you were going to do a .vacuous method for coverage type use. I am
>more interested in the .pending method as a way of simplifying properties
>by removing some necessary and complex modeling code...
>
>The idea of the .pending method is for cases where one want to limit the
>number
>of started sequences to either one or a fixed amount. E.g.
>
>property only_one;
> (<req_level> && !only_one.pending() ##1 !retry |-> ##[1:10] done ##0
> check);
>endproperty
>
>Alternative modelings have to duplicate the equation of <req_level> and
>maintain a 2 state FSM and properly model the ending of the property.
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic Corp.
> Plano TX. 75074
>
>
>-------- Original Message --------
>Subject: Re: Supporting general case of assertion functions and .ended/matched
>Date: Thu, 13 Nov 2003 22:12:55 -0500
>From: Surrendra Dudani <Surrendra.Dudani@synopsys.com>
>To: Adam Krolnik <krolnik@lsil.com>
>References: <5.1.0.14.2.20031107110632.01d3f128@us04.synopsys.com>
><3FAABCC4.3070207@lsil.com> <200311061822.hA6IMoZ21566@tamale.sps.mot.com>
><3FAABCC4.3070207@lsil.com>
><5.1.0.14.2.20031107110632.01d3f128@us04.synopsys.com>
>
>Hi Adam,
>Please review the proposal on the extension of the temporal functions($past
>etc.) that I sent today. For others issues, please see comments below.
>Surrendra
>At 04:37 PM 11/10/2003 -0600, you wrote:
>
>
>>Hi Surrendra;
>>
>>It appears that SV-EC will be moving up the review of the reacting to
>>assertions enhancement of Arturo's.
>>
>>I wanted to write up my request for merging Arturo's method calls used
>>in waiting and detecting assertion occurrences.
>>
>>I however wanted to see what you would write about the functions ($past,
>>etc.)
>>and method calls for the general form. This would be the basis, I think,
>>for reacting to assertions.
>
>This is available now.
>
>>Arturo proposed:
>>
>>.triggered as a way to detect an property occurrence.
>>
>>I would like to see this merged with ".ended" as they appear to be the same
>>idea.
>
>We thought quite a bit about this, but decided to keep the two methods.
>Although their functionality overlaps "in spirit", merging the two caused
>other problems, such as
>1) Detecting the end of sequences using @ operator implies that the end of
>sequence "generates" an event. So triggered seems applicable.
>2) The use of ended in sequences as well as in the code can cause confusion
>about its semantics, since ended have a special treatment in sequences.
>Sequences using ended are automatically ordered to get the correct results.
>Cyclic use of ended is not allowed, etc.
>3) Formal semantics for ended can only be partially defined for its use in
>sequences
>
>Once we modeled the end of sequence as an event, then all the other
>definitions are already provided for in SV.
>
>>I would also like to see two additional method calls:
>>
>>".vacuous" - I think we talked about this for coverage - to see
>>sequences/events
>> that occur, but not vacuously.
>>
>>".pending" - To report how many pending or in progress threads of execution a
>> particular property has.
>>
>>This ".pending" method simplifies the need to maintain state to prevent
>>another
>>thread of execution from beginning. I believe you have seen this type of
>>code in implementing some of the ova blocks and the OVL blocks. I have seen
>>this as well and request the return of "how many execute". This allows one to
>>prevent another execution, and to limit the number of executions. E.g.
>>
>>property only_once;
>> (starting && !only_once.pending() |-> ... );
>>endproperty
>>
>>property less_than_5;
>> (starting && less_than_5.pending < 5 |-> ... );
>>endproperty
>>
>>or.
>>
>>assert property (less_than_5.pending < 5)
>> else $error("Exceeding dispatch depth on XXX interface.");
>
>These are good ideas, however, we are running out of time to define them
>precisely. If you can come up with a definition, I would be willing to
>support it.
>
>> Thanks.
>>
>> Adam Krolnik
>> Verification Mgr.
>> LSI Logic Corp.
>> Plano TX. 75074
>> Co-author "Assertion Based Design"
>>
>
>
>
>**********************************************
>Surrendra A. Dudani
>Synopsys, Inc.
>377 Simarano Drive, Suite 300
>Marlboro, MA 01752
>
>Tel: 508-263-8072
>Fax: 508-263-8123
>email: Surrendra.Dudani@synopsys.com
>**********************************************
>
>
**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive, Suite 300
Marlboro, MA 01752
Tel: 508-263-8072
Fax: 508-263-8123
email: Surrendra.Dudani@synopsys.com
**********************************************
This archive was generated by hypermail 2b28 : Fri Nov 14 2003 - 08:25:59 PST