RE: [sv-ac] reminder to vote on mantis 1550

Hi Arturo,

I think that the initialization behavior should be deterministic and
this is important at least for assertion modeling. I am preparing a
separate proposal about the assertion modeling, where I suggest using
different simulation semantics for assertion modeling constructs. Until
this enhancement has been introduced formal verification people use SV
RTL for this purpose, and therefore the initialization in FV and
simulation should agree.

As for $past beyond the start of the simulation, its deterministic
definition is absolutely necessary. This is the only mean in FV to
specify the initial condition in an assertion. We rely on the fact that
$past(a) = 0 at the simulation beginning for two-value variables. Here
is an example: if initially two variables were mutex then the third
variable will eventually be set:

assert property (@(posedge clk) !$past(1) && $onehot0({a, b}) |->
##[0:$]c);

The check for "initially" is done using !$past(1): $past(1) is always 1
except for the initial moment where it is 0. This example may easily be
scaled to arbitrary properties.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Arturo Salz
Sent: Friday, January 26, 2007 11:55 PM
To: Rich, Dave; john.havlicek@freescale.com; Eduard.Cerny@synopsys.com
Cc: sv-ac@server.eda-stds.org
Subject: RE: [sv-ac] reminder to vote on mantis 1550

Dave,

I agree.

That paragraph implies that sampling a variable initialized in its
declaration may behave differently from a wire that is initialized at
the start of simulation - such as the target of a continuous assignment
of a constant value, or a constant port value. As I said before,
sampling at time zero or using $past beyond the start of the simulation
need not behave in a deterministic manner - just follow the rules set
forth by the LRM. Users should be cautioned against using 0 time
sampling.

	Arturo

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Rich, Dave
Sent: Friday, January 26, 2007 7:44 AM
To: john.havlicek@freescale.com; Eduard.Cerny@synopsys.COM
Cc: sv-ac@eda-stds.org
Subject: RE: [sv-ac] reminder to vote on mantis 1550


6.4 says "In SystemVerilog, setting the initial value of a static
variable as part of the variable declaration (including static class
members) shall occur before any initial or always blocks are started."

The is no definition of "before time 0"


> -----Original Message-----
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org]
On
> Behalf Of John Havlicek
> Sent: Friday, January 26, 2007 7:32 AM
> To: Eduard.Cerny@synopsys.com
> Cc: john.havlicek@freescale.com; Eduard.Cerny@synopsys.com; sv-
> ac@server.eda-stds.org
> Subject: Re: [sv-ac] reminder to vote on mantis 1550
> 
> Hi Ed:
> 
> I think we should not be clarifying Section 9.  I think we
> should ask whoever is responsible for Section 9 to do the
> clarification, although we can send them suggestions.
> 
> Do you agree that declaration assignments are executed as
> part of
> 
>    initialize the values of all nets and variables
> 
> ?  If not, then this certainly needs clarification.
> 
> Do we all agree that the initial blocks are not a part
> of this and that they get scheduled in the active region
> of the time 0 slot?
> 
> J.H.
> 
> > X-MimeOLE: Produced By Microsoft Exchange V6.5
> > Content-class: urn:content-classes:message
> > Date: Fri, 26 Jan 2007 07:22:32 -0800
> > Thread-Topic: [sv-ac] reminder to vote on mantis 1550
> > Thread-Index: AcdBW9xQw8waBr6YTHqAutCt1fwOeAAAaMcg
> > From: "Eduard Cerny" <Eduard.Cerny@synopsys.com>
> > Cc: <sv-ac@eda-stds.org>
> > X-OriginalArrivalTime: 26 Jan 2007 15:22:33.0619 (UTC)
> FILETIME=[CD57B630:01C7415D]
> >
> > Hi John,
> >
> > I agree that this is what should happen, but as you say yourself, it
is
> > not stated in the algorithm. Should we add that there? Or in 1550
just
> > for the sampled value fncts? I'd still like to add that that result
of
> > initializationa nd evaluation sets values that can be thought of as
> > being valid from -oo till 0-.
> >
> > ed
> >
> >  =20
> >
> > > -----Original Message-----
> > > From: John Havlicek [mailto:john.havlicek@freescale.com]=20
> > > Sent: Friday, January 26, 2007 10:08 AM
> > > To: Eduard.Cerny@synopsys.COM
> > > Cc: john.havlicek@freescale.com; Eduard.Cerny@synopsys.COM;=20
> > > sv-ac@eda-stds.org
> > > Subject: Re: [sv-ac] reminder to vote on mantis 1550
> > >=20
> > > Hi Ed:
> > >=20
> > > I never said anything got scheduled into the preponed region.
> > >=20
> > > Look at the scheduling algorithm.  The step
> > >=20
> > >   initialize the values of all nets and variables
> > >=20
> > > executes before the execution of the time 0 slot begins.  My
> > > interpretation is that this step includes execution of the=20
> > > declaration assignments.
> > >=20
> > > The value of an expression should be readable in the=20
> > > preponed region.  What I am saying is that if an expression
> > > is read (or sampled) in the preponed region of the time 0 slot,
> > > then it should see the effects of the=20
> > >=20
> > >   initialize the values of all nets and variables
> > >=20
> > > In other words, the declaration assignments are reflected in=20
> > > the preponed values in the time 0 slot.
> > >=20
> > > Do you disagree?
> > >=20
> > > J.H.
> > >=20
> > >=20
> 
> --


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.



-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.