Re: [sv-ac] Review of 3033

[3033] Statements and constructs within a checker that are sensitive to
changes (e.g., clocking events, continuous assignments), and all blocking
statements are scheduled in the Reactive region (similarly to programs, see
24.3.1).

However, [p1800, 17.3.1 Behavior of instantiated checkers] Immediate
assertions, including deferred assertions, are handled normally as described
in 16.3 and 16.4.
[16-2] Immediate assertions follow simulation event semantics for their
execution and are executed like a
statement in a procedural block.
[Ben] Thus, regular and deferred assertions in an always_comb are also
executed in the Reactive region. Are there any differences between regular
and deferred assertions in checkers?
Ben

On Mon, May 30, 2011 at 1:14 AM, Korchemny, Dmitry <
dmitry.korchemny@intel.com> wrote:

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

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.