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

Hi Hillel:

> Adding assigned declarartion to determine the $sampled initial result
> complicates things, because there is no equivalent to "outer module
> assignment" for an assigned declaration.

Apparently you do not agree with my argument that deleting any
statement that defines special treatment of $sampled in the time 0 
slot is simpler.

How do you explain that when there is no change to the variables 
in the argument to $sampled, there is still a change in the value
returned by $sampled from the time 0 slot to the time 1 slot?

Also, if there were an assertion that is checked in the time 0 slot,
it would use the preponed values, which would not longer be equal
to the values returned by $sampled in the time 0 slot.  Therefore,
we would not be able to say that $sampled is redundant within assertion
boolean expressions because it simply would not be true.

Regarding the external control of the preponed values in the time 0 
slot for the purpose of creating simulation replays of model checking
counterexamples, there may be a need for this, but I think that
it is separate from the definition of $sampled.  If you can control
the preponed values, then $sampled should return them to you.  

J.H.

> Content-class: urn:content-classes:message
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> X-OriginalArrivalTime: 26 Jan 2007 07:05:44.0625 (UTC) FILETIME=[65CC3210:01C74118]
> Date: Fri, 26 Jan 2007 00:05:39 -0700
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] reminder to vote on mantis 1550
> Thread-Index: AcdAs0bTcrq7EThTRdmyhL1bD8l4HQADUOkgABUqu7A=
> From: "Miller Hillel-R53776" <r53776@freescale.com>
> Cc: <sv-ac@eda-stds.org>
> 
> Ed,
> 
> The wording is good.
> 
> There still is a missing capability to allow one to initialize the first
> $sampled of a variable/register.=20
> 
> There is a need for this when producing a simulation vector set that
> needs to reflect a specific behaviour. The behaviour can be influenced
> by the initial values of the $sampled function on a specific expression.
> In the model checking domain this becomes more important because model
> checking produces counter examples where a key element of the counter
> example is the initial state.
> 
> Up to now the initial state for a counter example can be determined by
> referencing an internal register from an outer module assignment.=20
> 
> Adding assigned declarartion to determine the $sampled initial result
> complicates things, because there is no equivalent to "outer module
> assignment" for an assigned declaration.
> 
> The initilization sequence of model checking tools are very subtle
> because they use "simulation semantics" to initialize what they can and
> then they move to the model checking phase. States that were not
> initialized get their values picked to satisfy the counter example.
> 
> I think the root request is for an ability to do an out of module
> assignment that will be executed at the same time the assignment
> declaration is done. This should be done by the committee that provided
> the declaration assignment capability.
> 
> Judgement needs to be made whether we need this for the completeness of
> 1550.
> 
> Thanks
> Hillel
> 
> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
> Eduard Cerny
> Sent: Thursday, January 25, 2007 10:38 PM
> To: Havlicek John-r8aaau; Eduard.Cerny@synopsys.com
> Cc: sv-ac@eda-stds.org
> Subject: RE: [sv-ac] reminder to vote on mantis 1550
> 
>  Hi John,
> 
> before I deposit it on mantis, would the wording in the attached updated
> proposal be acceptable?
> 
> Thanks,
> ed
> 
> > -----Original Message-----
> > From: John Havlicek [mailto:john.havlicek@freescale.com]
> > Sent: Thursday, January 25, 2007 2:02 PM
> > To: Eduard.Cerny@synopsys.COM
> > Cc: john.havlicek@freescale.com; sv-ac@eda-stds.org
> > Subject: Re: [sv-ac] reminder to vote on mantis 1550
> >=20
> > Hi Ed:
> >=20
> > I think so, at least as a friendly ammendment, because we should not=20
> > allow the inconsistency between 1. and 2. that I pointed out in a=20
> > previous mail.
> >=20
> > I am happy to leave the ballot ongoing unless you feel that we ought=20
> > to abort it, revise the proposal, and later call for a new vote.
> >=20
> > I think we need to get a clearer idea of the missing capability Hillel
> 
> > is talking about before suggesting anything else.
> >=20
> > J.H.
> >=20
> > > X-MimeOLE: Produced By Microsoft Exchange V6.5
> > > Content-class: urn:content-classes:message
> > > Date: Thu, 25 Jan 2007 10:45:41 -0800
> > > Thread-Topic: [sv-ac] reminder to vote on mantis 1550
> > > Thread-Index: AcdAsKlMvCOtBXb4Q8iSQbCdS8ayaAAAE7kg
> > > From: "Eduard Cerny" <Eduard.Cerny@synopsys.com>
> > > X-OriginalArrivalTime: 25 Jan 2007 18:45:42.0050 (UTC)
> > FILETIME=3D[03CCF020:01C740B1]
> > >=20
> > > Hi John,
> > >=20
> > > should I change the proposal along these lines?
> > >=20
> > > ed=3D20
> > >=20
> > > > -----Original Message-----
> > > > From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On=3D20 =20
> > > >Behalf Of John Havlicek
> > > > Sent: Thursday, January 25, 2007 1:40 PM
> > > > To: sv-ac@eda-stds.org
> > > > Subject: Re: [sv-ac] reminder to vote on mantis 1550 =3D20  Hi Ed:
> > > >=3D20
> > > > I think tha what you describe will achieve consistency =
> between=3D20=20
> > > >=3D20  1. $sampled returns the preponed value of its argument in=20
> > > >the=3D20
> > > >    current time slot (including the time 0 slot).
> > > >=3D20
> > > > and=3D20
> > > >=3D20
> > > > 2. What the LRM currently says about preponed values in the=3D20
> > > >    time 0 slot.
> > > >=3D20
> > > >=3D20
> > > > Hillel has indicated that there are still missing capabilities, =20
> > > >but I'm not sure that these should be addressed by changing  the=20
> > > >definition of $sampled.=3D20 =3D20  J.H.
> > > >=3D20
> > > > > X-MimeOLE: Produced By Microsoft Exchange V6.5
> > > > > Content-class: urn:content-classes:message
> > > > > Date: Thu, 25 Jan 2007 06:44:39 -0800
> > > > > Thread-Topic: [sv-ac] reminder to vote on mantis 1550
> > > > > Thread-Index: AcdAIjfrqD0yBNyUSJKs6kNGFbt2agAZnDewAAGZvdA=3D3D
> > > > > From: "Eduard Cerny" <Eduard.Cerny@synopsys.com>
> > > > > X-OriginalArrivalTime: 25 Jan 2007 14:44:40.0972 (UTC)=3D20
> > > > FILETIME=3D3D[58538CC0:01C7408F]
> > > > >=3D20
> > > > > Hi, would it be enough to change the text so that it is
> > the value
> > > > > assigned in the declaration of the variable or in the
> > absence the
> > > > > default value of type? I view the assigned values in=3D20
> > > > declarations and
> > > > > the default values as the values that the variable has
> > from -oo till
> > > > > 0^-.
> > > > >=3D20
> > > > > ed=3D3D20
> > > > >=3D20
> > > > >> -----Original Message-----
> > > > >> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] =
> On=3D3D20
> 
> > > > >>Behalf Of Miller Hillel-R53776
> > > > >> Sent: Thursday, January 25, 2007 9:24 AM
> > > > >> To: Havlicek John-r8aaau; sv-ac@eda-stds.org
> > > > >> Subject: RE: [sv-ac] reminder to vote on mantis 1550 =3D3D20 =20
> > > > >>John, =3D3D20  I am not sure we should make such an =
> inconsistency=20
> > > > >>it
> > sounds=3D3D20
> > > > >> troubling.
> > > > >>=3D3D20
> > > > >> However, the reason why static variable declarartion=3D3D20 =20
> > > > >>assignments cannot  be used, is that it cannot be used by an=20
> > > > >>outer module=3D20
> > > > reference. If I
> > > > >> want to influence the initial value of a $ function
> > that is=3D3D20
> > > > >> dependent on
> > > > >> a module's reg, how would this be done. Would I need to=3D3D20  =
> 
> > > > >>rewrite the code  with the declaration assignment?
> > > > >>=3D3D20
> > > > >> Maybe we need an additional construct for initializing
> > the $sampled
> > > > >> value of a variable at the same time as assignment declaration.
> > > > >>=3D3D20
> > > > >> Thanks
> > > > >>=3D3D20
> > > > >>=3D3D20
> > > > >> =3D3D20
> > > > >>=3D3D20
> > > > >>=3D3D20
> > > > >> Hillel Miller>
> > > > >>=3D3D20
> > > > >>=3D3D20
> > > >=3D20
> > > > --=3D20
> > > > This message has been scanned for viruses and  dangerous content=20
> > > >by MailScanner, and is  believed to be clean.
> > > >=3D20
> > > >=3D20
> >=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.