RE: [sv-ac] Review of 3033

Hi Tom,

Please, see my comments below.

Thanks,
Dmitry

-----Original Message-----
From: Thomas J Thatcher [mailto:thomas.thatcher@oracle.com]
Sent: Friday, June 03, 2011 19:57
To: Korchemny, Dmitry
Cc: sv-ac@eda.org
Subject: Re: [sv-ac] Review of 3033

Hi Dmitry,

On 05/30/11 01:14, Korchemny, Dmitry wrote:

> 17.5 Checker procedures
>
> Why not make all procedural assignments use current values, not
> sampled values? Then have assertions use the sampled values of all
> deterministic checker variables. This would be much more regular.
>
> [Korchemny, Dmitry] See my comment at the beginning.
>
> It would also fix your example: both a (the checker input) and x (the
> checker variable assigned in the always_ff) would use the sampled
> value, and the assertion would return the same value, no matter
> whether clk changes in the Active region (from RTL code) or the
> Reactive region (from the test bench).
>
> [Korchemny, Dmitry] Are you assuming that checker inputs are sampled? This is problematic even now for deferred assertions (see the preamble), and will also kill continuous and blocking assignments introduced in this proposal.
>
No, you are correct. The RHS expressions of non-blocking assignments need to be sampled. However, I would still suggest that concurrent assertions use the sampled values of the deterministic checker variables. In most cases it doesn't matter. But if anyone tries to derive a clock inside the checker, then the assertions would see consistent values, even though the assertions are evaluated in the second pass through the Observed region.
[Korchemny, Dmitry] This is fine. Both in the existing LRM and in my proposal the deterministic checker variables are sampled in concurrent assertions.

> Random checker variables would still be assigned in the beginning of
> the Observed region, and assertions would use the current values of
> these variables. In the case of Random assignments, the assume
> properties that determine the values chosen would use the sampled
> values of both the checker inputs, the deterministic checker
> variables, and of XMRs that are referenced. So the result would be
> consistent, no matter how many times we go around the "big loop"
> before we assign the random checker variables. This would also mean
> that we wouldn't need to get multiple values for random checker
> variables, even if they are solved multiple times in one time-step.
>
>
> 17.7.3
> I'm not sure whether we should put this example in or not. There's no
> way we could document all the different ways users could cause
> problems for themselves.
>
> [Korchemny, Dmitry] If I remember correctly, somebody asked me to insert this example. Let's discuss its usefulness in the meeting.
>
Should it be an error for a random variable to be constrained by assume property constructs with different clocks? It seems troubling that a random variable would be solved multiple times in one time step.

[Korchemny, Dmitry] I suggest to allow this. Even when a random variable is constrained by several assumptions with the same clock, unless the simulator performs some global analysis, the random variable will also be solved multiple times. Essentially the simulator is not required to solve all the imposed constraints correctly. Therefore, even the following dumb algorithm is correct: solve the first assumption, and check the solution against the second assumption: in the worst case the second assumption will fail.

Here is an example when constraining a free variable with assumptions with different clocks is useful:

We want a read request to behave as follows:
* It cannot be issued simultaneously with the write request on the rising edge of some clock (this assumption is governed by posedge clk)
* Its value should remain stable between two consecutive ticks of clk (this assumption is governed by $global_clock).

> Tom
>
---------------------------------------------------------------------
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.