Subject: Re: Fw: [sv-ec] Re: $wait_all/any/...
From: dudani@us04.synopsys.com
Date: Fri Jan 10 2003 - 13:07:15 PST
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.
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
> >----- 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 : Fri Jan 10 2003 - 13:08:15 PST