RE: [sv-ac] New version of 3213 uploaded

From: Little Scott-B11206 <B11206@freescale.com>
Date: Thu Apr 14 2011 - 04:56:55 PDT

Hi Dmitry:

I think you are asking for trouble if you remove $sampled from the LRM. I don't know if I was present in the meeting where you mentioned deprecating it, but I don't think it is a good idea to deprecate $sampled right now. Maybe down the road that idea can be entertained, but I would not support deprecating $sampled right now.

Thanks,
Scott

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
> Korchemny, Dmitry
> Sent: Thursday, April 14, 2011 4:15 AM
> To: thomas.thatcher@oracle.com
> Cc: sv-ac@eda-stds.org
> Subject: RE: [sv-ac] New version of 3213 uploaded
>
> Hi Tom,
>
> I don't think that this proposal resurrects the sampling semantics: the
> sampling semantics remained exactly as it was. My initial proposal was
> indeed to change the definition of sampling, e.g., to say that a
> sampled value of an automatic variable is its current value. The
> objection expressed by you and Gord in the F2F was that we were abusing
> the term "sampling" and that it would be confusing to call a value
> sampled when it is actually not. Therefore I am introducing a new
> concept of a concurrent context.
>
> Please, see my specific comments below.
>
> Thanks,
> Dmitry
>
>
> -----Original Message-----
> From: Thomas J Thatcher [mailto:thomas.thatcher@oracle.com]
> Sent: Thursday, April 14, 2011 02:41
> To: Korchemny, Dmitry
> Cc: sv-ac@eda-stds.org
> Subject: Re: [sv-ac] New version of 3213 uploaded
>
> Hi Dmitry,
>
> I read through the proposal for 3213, and I really don't think this is
> the way we want to go. This proposal resurrects the sampling semantics
> that we rejected at the face-to-face, but calls them concurrent
> semantics rather than sampled semantics.
>
> I especially don't like the fact that the $sampled function is
> completely deleted from the standard. The changes to 20.13 delete the
> $sampled function from the BNF. This would be a huge backward
> compatibility headache for us. This would require that we touch every
> single assert file we have ever written.
>
> [Korchemny, Dmitry] The previous version of this proposal retained the
> function $sampled. In one of our recent meetings I was asked to
> deprecate the function $sampled, and no objections were expressed. This
> is what I did in the later versions. And indeed, I could not find any
> real life use case where the function $sampled would be the right
> choice. Do you have any supporting example in mind?
>
> The current definition of sampling works for just about everything.
> - Design variables are sampled.
> - Checker variables (non-random) don't really need to be sampled,
> because they change after the Observed region, but sampling them
> doesn't hurt.
> Simulators could do optimization internally to skip the sampling
> of these variables if that helped performance.
>
> [Korchemny, Dmitry] Non-blocking checker variables do need to be
> sampled since if their value may change several times in the same
> timestep.
>
> The only thing that doesn't work are random checker variables, because
> they are assigned in Observed, and used in Observed.
>
> [Korchemny, Dmitry] I disagree: there are many exceptions from the
> sampling rule, including local and automatic variables, sequence method
> results, and free checker variables.
>
> I am OK with defining a $concurrent function, for the special cases
> where it might be needed, but I don't want to re-write the whole LRM to
> remove all references to sampling.
>
> [Korchemny, Dmitry] I don't see a feasible alternative.
> Many statements in the LRM are simply wrong when talking about sampled
> values. Here are some examples:
> * In an assertion, the sampled value is the only valid value of a
> variable at a clock tick.
> * The sampled values are used to evaluate ... Boolean subexpressions
> that are required to determine a match of a sequence.
> * The Boolean expressions used in defining a sequence or property
> expression shall be evaluated over the sampled values of all variables
> (other than local variables as described in 16.10) and the current
> values of local variables and of the sequence Boolean methods triggered
> and matched (see 16.14.6).
> 16.9.3
> * The use of $sampled in assertions, although allowed, is redundant, as
> the result of the function is identical to the sampled value of the
> expression itself used in the assertion.
> etc.
>
> Also it seems like you are asking
> the compiler writers for magic, if you expect to pass an expression and
> have the function use the sampled value of the first variable in that
> expression, the current value of the second variable, and the sampled
> value of the third.
>
> [Korchemny, Dmitry] I am not asking anything different from what we
> have today: if you have in some assertion the following expression:
> a[i] & b & seq.triggered
> Where i is an automatic variable, b is a design variable, and seq is a
> sequence, the current values of i and seq.triggers and the sampled
> value of b will be taken.
> Also, what happens now when you pass an expression as an actual
> argument to a checker?
> There might be, indeed, some additional work to compiler writers if
> somebody decides to write something like
> assign c = $concurrent(a & b), where a is a design variable and b is an
> automatic one. But this should be doable as it is doable in assertions,
>
> Keep in mind that most assertions are written for simulation. These
> assertions will probably not use any random checker variables. Any
> changes we make will need to be transparent to these users.
>
> [Korchemny, Dmitry] How is this related? This proposal is relevant for
> simulation not less than for formal verification. Thus, automatic
> variables and embedded assertions are relevant mostly for simulation.
> The changes are absolutely transparent to the users since only the
> terminology has changed. Even if the users have an implicit invocation
> of function $sampled in their code, it will continue to work, since the
> deprecation does not forbid its use.
>
> Tom
>
> On 04/12/11 02:19, Korchemny, Dmitry wrote:
> > Hi all,
> >
> >
> >
> > I uploaded a new version of 3213 incorporating the reviewers'
> comments:
> > http://www.eda-
> stds.org/mantis/file_download.php?file_id=4909&type=bug
> > <http://www.eda-
> stds.org/mantis/file_download.php?file_id=4909&type=bug>.
> >
> >
> >
> > Thanks,
> >
> > Dmitry
> >
> > ---------------------------------------------------------------------
> > Intel Israel (74) Limited
> >
> > This e-mail and any attachments may contain confidential material for
> > the sole use of the intended recipient(s). Any review or distribution
> > by others is strictly prohibited. If you are not the intended
> > recipient, please contact the sender and delete all copies.
> > --
> > This message has been scanned for viruses and
> > dangerous content by *MailScanner* <http://www.mailscanner.info/>,
> and is
> > believed to be clean.
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
>
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
>
>
> --
> 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.
Received on Thu Apr 14 04:57:22 2011

This archive was generated by hypermail 2.1.8 : Thu Apr 14 2011 - 04:57:27 PDT