Subject: Re: Fw: [sv-ec] Re: $wait_all/any/...
From: Kevin Cameron x3251 (Kevin.Cameron@nsc.com)
Date: Mon Jan 13 2003 - 15:16:19 PST
> From Surrendra.Dudani@synopsys.com Mon Jan 13 07:42:47 2003
>
> 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
You can always consider events as ordered with respect to each other, I'm
not seeing what the problem is here.
Can you give an example?
Kev.
> 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
> > > **********************************************
This archive was generated by hypermail 2b28 : Mon Jan 13 2003 - 15:17:52 PST