RE: [sv-ac] Call to vote. Due August 30 (reminder)

Hi Tom,

I think that the confusion this solution involves less problems than the current behavior, as explained in the motivation section of 3035. Your code may be remedied if desired as

a11: assert #0 ($sampled(x));

However, let's consider the usage of this checker to understand the scope of the problem. Unlikely that this specific checker is designed to be procedural, since it contains an always procedure, and the execution of this procedure does not account conditions of the control statements in whose scope this checker is instantiated, were it instantiated in a procedural context. If so, there is almost no difference between a1 and a11: saying that the value is always true and that the sampled value is always true, is essentially the same thing. Therefore, it looks like that we don't have a serious problem here.

Keeping the current definition is problematic, it has many serious issues listed in the motivation section of proposal 3035.

Making everything in checkers non-sampled is also problematic. Let alone much more major backward compatibility issues that it will introduce, sampling in checker variable assignments is important.

Consider the following toy example (the transactions are assumed to be non-overlapped):

checker check_trans(in, out, start, complete, clk = $inferred_clock);
    default clocking @clk; endclocking

    type(in) data;
    always @clk
         data <= start ? in : data;

    a1: assert property (start ##1 complete[->1] |-> out = data);
endchecker

We want the assignment to be synchronized with the assertion, and the values in the RHS of the assignment should therefore be sampled: we want to use the value of "in" that was at the time when start was sampled in the assertion. If "in" and "start" are not sampled, the assertion and the modeling code could be inconsistent.
As for "data" itself is concerned, its value does not need to be sampled: in the RHS of the assignment its sampled value and its non-sampled value coincide, and the assertion is evaluated before data is modified in the Re-NBA region. Using non-sampled values of checker variables is more convenient since this is consistent with checker free variables which are not sampled.

Since one of the main goals of the checker is to contain modeling code for concurrent assertions, we need to support sampling in checker variable assignments.

Thanks,
Dmitry

-----Original Message-----
From: Thomas J Thatcher [mailto:thomas.thatcher@oracle.com]
Sent: Monday, August 30, 2010 7:38 PM
To: Korchemny, Dmitry
Cc: sv-ac@eda.org
Subject: Re: [sv-ac] Call to vote. Due August 30 (reminder)

What about the following case?

     checker check(x, clk);
         logic y;
         a1: assert #0 (x);

        always @clk begin
            y <=x;
        end

     endchecker

It seems that according to this proposal, the deferred assertion would
use the current value of x, while the assignment to the checker variable
y would use the sampled value. This could create confusion.

It seems that the only way to create a truly consistent semantics is one
of two choices: either keep the current semantics: all input arguments
to a checker are sampled. Or, remove all sampling semantics from
checker arguments. Variables inside a checker would then be sampled or
not sampled according to the rules which apply everywhere else.

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.