Subject: [sv-ec] Re: discrete time
From: dudani@us04.synopsys.com
Date: Tue Jan 14 2003 - 12:38:22 PST
Delta cycles are not quantized, and not part of the language. You cannot
refer to a delta cycle.
Surrendra
At 12:28 PM 1/14/2003 -0800, you wrote:
> > From Surrendra.Dudani@synopsys.com Tue Jan 14 12:19:36 2003
> >
> > If two events occur within the same time unit, we can refer to their
> > occurrence in certain order. However, there is no way to quantify the time
> > within a time unit. Assertions require quantified time.
> > Surrendra
>
>You can count delta cycles within a tick if you need to. From a logical
>standpoint all times are relative, there is no real need to differentiate
>between a tick and a delta.
>
>Kev.
>
>
> > At 10:52 AM 1/14/2003 -0800, you wrote:
> > > > From Surrendra.Dudani@synopsys.com Tue Jan 14 08:34:40 2003
> > > >
> > > > The semantics of verilog events do not fit in the assertion semantics
> > > being
> > > > considered, as assertion semantics require discrete time.
> > >
> > > > Surrendra
> > >
> > >Can you point me at your definition of "discrete time" since by the
> > >Verilog-AMS
> > >LRM all Verilog[-D] is discrete.
> > >
> > >Kev.
> > >
> > > > At 03:16 PM 1/13/2003 -0800, you wrote:
> > > > > > 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
> > > > > > > > **********************************************
**********************************************
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 : Tue Jan 14 2003 - 12:40:30 PST