Re: [sv-ac] Review of 3033

One more thing:
[3033] ● A checker variable may not be assigned in an
*initial*procedure. For example:

*bit *v;**

*initial *v = 1'b0; // Illegal

[Ben]Is

bit w=1'b1; legal?

What's the difference between v and w? What's the rationale for v?

Ben

On Thu, Jun 9, 2011 at 9:09 PM, ben cohen <hdlcohen@gmail.com> wrote:

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