Subject: Re: Fw: [sv-ec] Re: $wait_all/any/...
From: dudani@us04.synopsys.com
Date: Mon Jan 13 2003 - 07:45:11 PST
Kevin,
The problem is that multiple ordered Verilog events can happen within a
time unit, so it cannot be considered discrete. These testbench features
refer to ordering of events whether they happen in the same time unit or not.
Surrendra
At 02:00 PM 1/10/2003 -0800, you wrote:
> > From: "dudani@us04.synopsys.com" <Surrendra.Dudani@synopsys.com>
> >
> > Hi Erich,
> > With PSL or SV assertions (under consideration in DWG), one can express
> > great many situations that resemble ordering. However, there are some
> > important differences:
> > 1) Both languages assume a notion of discrete time. Discrete time implies
> > sampled values. The version of LTL ( that includes next operator)
> > inherently uses discrete time.
>
> >From an Verilog-AMS (LRM) viewpoint all [System]Verilog is discrete. Time
>is quantized in all event driven simulators, hence all values are sampled.
>
> > 2) Neither one can use verilog events, as verilog events have no notion of
> > time. They are purely asynchronous. Both languages refer to the notion
> of a
> > tick or a clock cycle, where the values are sampled according to some
> rules.
> >
> > To support pure asynchronous events, which do not relay on any notion of
> > time or clock, one would need different logic using timed-automata, which
> > is quite complex and not supported by most commercial formal tools. The
> > semantics also would be very different.
> >
> > The functionality discussed here for testbench related features has to do
> > with verilog events.
> > I hope that clarifies the need to keep it separate from assertions.
> >
> > Surrendra
>
>Can't you just consider the tick of the simulation kernel as a clock if
>there isn't anything else?
>Any syntax that handles event sequencing over indefinite numbers of cycles
>should work OK.
>
>Kev.
>
> > > >----- Original Message -----
> > > >From: "Erich Marschner" <erichm@cadence.com>
> > > >To: "Arturo Salz" <Arturo.Salz@synopsys.COM>; <mac@verisity.com>
> > > >Cc: <sv-ec@eda.org>
> > > >Sent: Tuesday, December 31, 2002 8:07 AM
> > > >Subject: RE: [sv-ec] Re: $wait_all/any/...
> > > >
> > > >
> > > >
> > > >Arturo,
> > > >
> > > >Your comment below:
> > > >
> > > >| The Accellera PSL effort will provide SystemVerilog with assertions
> > > >| and sequences. However, all the property languages on which it is
> > > >| based (Sugar, ForSpec, OVA) are strictly synchronous languages,
> > > >
> > > >is incorrect in two ways.
> > > >
> > > >First, it suggests that Accellera PSL is somehow based on ForSpec and
> > > >OVA. You know as well as I do
> > > >that this is at least misleading if not simply false. Accellera PSL is
> > > >based on Sugar, not on
> > > >ForSpec (which was rejected by the FVTC) or on OVA (which is
> essentially a
> > > >repackaging of ForSpec).
> > > >If you meant to say that Sugar, ForSpec, and OVA are all based on LTL,
> > > >that would be correct, but
> > > >that doesn't imply that Accellera PSL is based on ForSpec or OVA.
> > > >
> > > >Second, Accellera PSL is not a strictly synchronous language, as Bernard
> > > >pointed out. Unlike
> > > >ForSpec and OVA, Accellera PSL supports asynchronous assertions (clocked
> > > >or otherwise) in a
> > > >completely transparent fashion.
> > > >
> > > >Regards,
> > > >
> > > >Erich Marschner
> > > >Co-Chair, Accellera FVTC
> > > >
> > > >
> > > >-------------------------------------------
> > > >Erich Marschner, Cadence Design Systems
> > > >Senior Architect, Advanced Verification
> > > >Phone: +1 410 750 6995 Email: erichm@cadence.com
> > > >Vmail: +1 410 872 4369 Email: erichm@comcast.net
> > > >
> > > >| -----Original Message-----
> > > >| From: Arturo Salz [mailto:Arturo.Salz@synopsys.com]
> > > >| Sent: Friday, December 20, 2002 9:46 PM
> > > >| To: mac@verisity.com
> > > >| Cc: sv-ec@eda.org
> > > >| Subject: Re: [sv-ec] Re: $wait_all/any/...
> > > >|
> > > >|
> > > >| The Accellera PSL effort will provide SystemVerilog with assertions
> > > >| and sequences. However, all the property languages on which it is
> > > >| based (Sugar, ForSpec, OVA) are strictly synchronous languages,
> > > >| that is, each temporal statement in a sequence is sampled and
> > > >| evaluated using a particular clock (an event or an edge). This means
> > > >| that the entire sequence is synchronous to a clock. Verilog's event
> > > >| mechanism has no such limitation and neither would the wait_*
> > > >| constructs proposed. That is one distinction between the two
> > > >| approaches. Also, none of these assertion languages have a succinct
> > > >| syntax for specifying the strict ordering semantics of wait_order and
> > > >| they would have to be spelled out in a manner similar to my last
> > > >| message.
> > > >|
> > > >| I hope this helps clear things up.
> > > >|
> > > >| Arturo
> > > >|
> > > >| Happy Holidays to all.
> > > >|
> > > >| ----- Original Message -----
> > > >| From: "Michael McNamara" <mac@verisity.com>
> > > >| To: "Arturo Salz" <Arturo.Salz@synopsys.COM>
> > > >| Cc: <mac@verisity.com>; <sv-ec@eda.org>
> > > >| Sent: Friday, December 20, 2002 5:56 PM
> > > >| Subject: Re: [sv-ec] Re: $wait_all/any/...
> > > >|
> > > >|
> > > >|
> > > >| I must say it is much more enjoyable to engage in dialog with you,
> > > >| than with certain other folks...
> > > >|
> > > >| Thank you for you further explainiation of the distinction between
> > > >| wait_order and a simple @(a); @(b).
> > > >|
> > > >| With the further semantics of wait_order explained, I see it as being
> > > >| mush more similar to the property specification languages (sugar, e,
> > > >| Forspec, CBV) that have rich semantics for specifying sequences that
> > > >| behave as you describe; as well as allowing branches and recognizing
> > > >| bad sequences and killing a main sequence.
> > > >|
> > > >| Help me understand the game plan. Are we not going to get syntax for
> > > >| assertions and sequences from the Accellera PSL effort by virtue of
> > > >| the DWG?
> > > >|
> > > >| I apologize for perhaps not paying attention to some email where this
> > > >| was all coherantly explained.
> > > >|
> > > >| -- an aside --
> > > >|
> > > >| I want to wish Happy Holidays to all; I am, and I assume many of you
> > > >| are off for some end of year vacation. Please everyone, be careful
> > > >| out there. The snow will still be there when you arrive; drive
> > > >| conservatively. Arrive alive!
> > > >|
> > > >| -mac
> > > >|
> > > >| Arturo Salz writes:
> > > >| > Mac,
> > > >| >
> > > >| > Thanks for providing such a lucid and clear explanation of event
> > > >| > semantics. I have no problems with your "creative" syntax, it's
> > > >| > clear, concise, and, I believe, in the spirit of Verilog. I do
> > > >| > think that you misunderstood the exact semantics of wait-order.
> > > >| > When I wrote earlier that wait-order means strictly in that order,
> > > >| > I meant that all the events must occur in precisely that
> > > >| order, and
> > > >| > no event can occur out of order. If one were to express something
> > > >| > like wait_order(a, b, c, d) using the syntax you propose,
> > > >| we'd have
> > > >| > to write:
> > > >| >
> > > >| > @( a then ( b and not (c or d) ) then (c and not d) then d);
> > > >| >
> > > >| > Of course, I've just cooked up a whole lot of
> > > >| non-existent syntax but I hope
> > > >| > this helps to explain the semantics, and the reason why
> > > >| this construct is
> > > >| > so valuable. And, by the way, the assertions do
> > > >| > provide a very simple syntax for describing a sequence of events:
> > > >| > seq = a ## b ## c ## d; (or something like that)
> > > >| > But, the difference is that all those expressions are
> > > >| clocked, whereas the
> > > >| > events can be asynchronous.
> > > >| >
> > > >| > Arturo
> >
> >
> >
> >
> >
> > **********************************************
> > Surrendra A. Dudani
> > Synopsys, Inc.
> > 377 Simarano Drive
> > Suite 300
> > Marlboro, MA 01752
> >
> > Tel: 508-263-8072
> > Fax: 508-263-8123
> > email: 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: dudani@synopsys.com
**********************************************
This archive was generated by hypermail 2b28 : Mon Jan 13 2003 - 07:45:46 PST