Subject: [sv-ac] [Fwd: Re: Supporting general case of assertion functions and .ended/matched]
From: Adam Krolnik (krolnik@lsil.com)
Date: Fri Nov 14 2003 - 07:48:19 PST
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
**********************************************
This archive was generated by hypermail 2b28 : Fri Nov 14 2003 - 07:49:15 PST