Subject: Re: Fw: [sv-ec] Re: $wait_all/any/...
From: Kevin Cameron x3251 (Kevin.Cameron@nsc.com)
Date: Fri Jan 10 2003 - 14:00:12 PST
> 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 : Fri Jan 10 2003 - 14:01:04 PST