Subject: Re: [sv-ec] Re: discrete time
From: Jayant Nagda (Jayant.Nagda@synopsys.com)
Date: Wed Jan 15 2003 - 15:52:39 PST
Bernard,
It seems like you are selectively not aware of effort
going in SV-AC's Design Working Group in unifying and creating
single System Verilog Assertion language.
Overall System Verilog will provide assertion capabilities
for both simulation and formal tools which will be
re-usable across tools.
Anyone who have implemented event simulator will know:
Counting delta cycles and delta cycle semantics have been
a big performance hinderance in VHDL simulators. We continue
to have these VHDL wishes pushed on this discussions.
Instead any of us trying to educate you in responding to your
mis statements and clarify your confusions, may we suggest that
you read requirements for assertion and how SV-AC is
addressing those requirements : http://www.eda.org/sv-ac/hm ?
Jayant Nagda
Bernard Deadman wrote:
> With respect Surrendra, I think you should look at the Sugar 2.0 / PSL
> semantics document - you're on the committee so you certainly have access
> to it.
>
> My understanding, as Erich Marschner confirmed on December 31st, is "...
> Accellera PSL is not a strictly synchronous language.... Unlike ForSpec
> and OVA, Accellera PSL supports asynchronous assertions (clocked or
> otherwise) in a completely transparent fashion."
>
> It may well be true that the inadequate, lowest-common-denominator sub-set
> of ForSpec / OVA that's masquerading as an assertion language in
> SystemVerilog needs clocks, but the almost standardized Sugar 2.0 / PSL
> that spans both Formal Model checking and simulation-based verification
> DOES NOT!!!!
>
> Isn't it about time SystemVerilog had a REAL assertion capability? Will
> users thank us a decade from now for rushing out an LRM based on arbitrary
> decisions, that does not promote re-use between tools supporting two
> related Accellera standards?
>
> Regards
>
> Bernard
>
> At 01:22 PM 1/15/2003 -0500, dudani@us04.synopsys.com wrote:
> >There has been no need to support Verilog events for assertions.
> >Assertions, as currently defined, satisfy their requirements with the
> >current notion clocks.
> >Surrendra
> >At 12:58 PM 1/14/2003 -0800, you wrote:
> >> > From Surrendra.Dudani@synopsys.com Tue Jan 14 12:35:56 2003
> >> >
> >> > Delta cycles are not quantized, and not part of the language. You cannot
> >> > refer to a delta cycle.
> >>
> >> > Surrendra
> >>
> >>What's your definition of "quantized".
> >>
> >>We're defining extensions to the language, no reason we can't add counting
> >>deltas if it makes assertions more usable.
> >>
> >>Kev.
> >>
> >> > 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.
> >><snip>
>
> ====================================================================
> SDV Inc. 9111 Jollyville Rd, Suite 102, Austin, TX 78759 USA
> Phone: (512) 231-9806 xt 101 FAX: (512) 231-9807 Mobile: (512)
> 431-5126
> Email: bdeadman@sdvinc.com Website: www.sdvinc.com
This archive was generated by hypermail 2b28 : Wed Jan 15 2003 - 15:53:38 PST