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

Hi Dimitry,

Maybe we just disagree on this. Let me explain my position.

I don't believe it's possible for a simulator to accurately model the
effect of powering up a system, which is what we usually refer to as
time 0 setup or initialization. By its very nature, this is an analog
process that cannot take place in zero time. I believe that attempting
to force a deterministic simulation model, which is not possible in the
real system, may conceal actual bugs and lull engineers into a false
sense of security. In order to avoid such situations, a simulator should
be conservative - without being overtly pessimistic. In this case,
conservative should cause designers to not rely on pre-initialized nets
- consider that in reality even the power supplies may be changing at
time 0.

I also understand that formal tools require deterministic values in
order to perform their job, but surely even formal tools should avoid
active clocking edges at time 0. In my opinion that is a sound
methodology. This is partly the reason for assertions to include the
'disable iff' construct - so that assertions can be disabled during
reset (or startup time) when many false negatives are likely to occur.
I'd be interested to see how your proposed simulation semantics for
assertion modeling addresses this issue.

As for the deterministic behavior of $past and relying on the fact that
for a two-state variable a, $past(a) is 0 at the start of simulation -
which BTW is consistent with standard SystemVerilog - may also get you
into trouble. Consider, for example, another signal b, that is the
negation of a:
	assign b = !a;
At time 0 both a and b might both be 0 simultaneously such that a simple
check like, $onehot0({a,b}), may pass incorrectly - or $onehot({a,b})
would fail equally incorrectly. Also, your property is relying on the 0
initial state of a two-state variable. If, instead, a is a four-state
variable, which is initialized to X, the !past(1) check will fail -
negation of X is still X which is false. BTW, none of this invalidates
what you're trying to do with the initial value, as long as you don't
attempt to sample at time 0.

	Arturo

-----Original Message-----
From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] 
Sent: Monday, January 29, 2007 10:19 AM
To: Arturo Salz; Rich, Dave; john.havlicek@freescale.com;
Eduard.Cerny@synopsys.COM
Cc: sv-ac@eda-stds.org
Subject: 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.