RE: [sv-ac] Review of 3033

Hi Tom,

Please, see my comments below. I uploaded a new version with several minor changes: http://www.eda-stds.org/mantis/file_download.php?file_id=5116&type=bug.

Since you raised issues with the basic definitions I suggest also to discuss your comments in a meeting.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Thomas J Thatcher
Sent: Saturday, May 28, 2011 00:39
To: sv-ac@eda.org
Subject: [sv-ac] Review of 3033

Hello Everyone,

This is a review of Dmitry's proposal for 3033. This proposal would
1. Remove checker argument sampling.
2. Make checker non-blocking assignments use the sampled value of their
RHS.
3. Add always_comb always_ff and always_latch
4. Add continuous assignments.

Before I get into a detailed review of this proposal, let me throw out a
radical idea for discussion (since we are changing a bunch of stuff and
breaking backward-compatibility anyway . . .):

[Korchemny, Dmitry] Note, however, that except for deferred assertions in checkers is concerned, the backward compatibility is minimal in my proposal. The definition you propose introduces also substantial backward incompatibility for all checker constructs.

Would it make sense to move all checker procedural activity to the
active region set? i.e. move checker non-blocking assignments to the
NBA region and then implement checker continuous assignments in the
active region?

[Korchemny, Dmitry] There are several problems with doing that:
* NBA with active free checker variables in their RHS will not work as expected: they will use the stale value of these variables.
* It will be impossible to use sequence triggered method in the RHS of the checker variable NBA: at this time it is always 0.
* Probably, the most important is nondeterministic behavior of a checker had this definition been adopted. I have an example in my proposal. Copying it here for convenience:

"The reason for sampling expressions in always and always_ff procedures is to make checkers behave deterministically and not to depend on the order of process execution. Consider the following example:

checker check2(logic a, clk);
        logic x;
        always_ff @clk
                x <= a;
        a1: assert property (@clk a |=> x);
endchecker : check2

Because the values in always_ff procedures are sampled, the evaluation order is well defined: x is assigned the value of a that it had before the clock change. The assertion a1 passes in this case. Were the sampled values used in always_ff procedures as it is done in modules, two scenarios could be possible. If the clock changed first the results would be identical to the ones described above. If a changed first then x would have been assigned the new value of a, and the assertion a1 could fail."

---
Here's why I'm thinking this:
Many users are still using modules to implement their checking code. 
When coding a procedural block in a module, any procedural or continuous 
assignments will take place in the active and NBA regions.  Signals 
defined in these modules work the same way as any other signals.  In 
assertions, they are sampled according to the same rules as signals in 
any other module.
Suppose checkers worked this way:  Non-blocking assignments would take 
place in the NBA region.  Blocking and continuous assignments would take 
place in the active region.  None of the assignments would use sampled 
values.  Assertions would use sampled values of input arguments
It seems that this would be much more regular and well behaved.  We 
would not need all these rules for special cases about what variable s 
are sampled and which are not sampled.
[Korchemny, Dmitry] Unfortunately, this comes at a price of the checker determinism and ability of using in NBA such constructs as sequence triggered method and active free checker variables as I explained above. Note also, that even though the assignment semantics in checkers is defined differently than in a module, this difference is almost transparent to the user. All constructs act more intuitively using this definition.
---
Now, on to the proposal.
"-- If an actual argument contains any subexpression that is a const 
cast . . ."
	Is more expression needed here to explain that the checker argument 
will be used as a const cast?  Or is the fact that a checker is 
flattened out sufficient?
[Korchemny, Dmitry] I agree, there is no need delete the explanation. Restored it.
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.
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.
Tom
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, 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.