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.