[sv-ac] RE: Continuous assignments and checker variable sampling

Hi Dmitry:

Can you be more explicit about the badness condition when checker free
variables are mixed with testbench variables? Can you write a simple
example to illustrate it? What behavior do you want for this example?

Notice that the rules do not say when checker free variables should be
solved or when checker continuous assignments should be performed. They
only say that continuous assignments should be performed after solving
for free variables.

J.H.

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Korchemny, Dmitry
Sent: Thursday, November 18, 2010 1:41 AM
To: Havlicek John-R8AAAU; sv-ac@eda.org
Cc: Little Scott-B11206
Subject: [sv-ac] RE: Continuous assignments and checker variable
sampling

Hi John, Scott,

According to your suggestion free checker variables should be sampled
(in the Preponed region) in concurrent assertions, which is good. What
is worse, I think your definition has a problem when a concurrent
assumption imposed on checker free variables contains TB variables.

Thanks,

Dmitry

From: Havlicek John-R8AAAU [mailto:r8aaau@freescale.com]
Sent: Thursday, November 18, 2010 1:14 AM
To: Korchemny, Dmitry; sv-ac@eda.org
Cc: Havlicek John-R8AAAU; Little Scott-B11206
Subject: RE: Continuous assignments and checker variable sampling

Hi Dmitry:

We have thought some about this. We think that the following rules
should be followed:

1. Checker continuous assignments should use current values of
their righthand sides and happen after solving for checker free
variables.

2. Checker free variables should be solved using current values of
the non-free variables.

3. Checker assumes should be checked using sampled values, just
like checker asserts.

We think that with these rules, the inconsistencies and insanities will
be reduced or, perhaps, eliminated. We have done a little bit of brain
simulation with the following code (which is like your code, but with
fewer negations):

checker check (bit a, event clk);

   default clocking @clk; endclocking

   rand bit v;

   bit w, b;

   m1: assume property ($onehot0({a, v});

   assign w = v;

   assign b = a;

   a1: assert property ($onehot0({a, w});

   a2: assert property ($onehot0({b, v});

   sanity1: assert property (w == v);

   sanity2: assert property (b == a);

endchecker : check

The rules seem to cause all the asserts and assumes to pass whenever
they are checked. We think that the sanity asserts are important for
intuitive behavior of checker continuous assignment.

Best regards,

  J.H. & S.L.

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Korchemny, Dmitry
Sent: Wednesday, November 17, 2010 9:13 AM
To: sv-ac@eda.org
Subject: [sv-ac] RE: Continuous assignments and checker variable
sampling

Hi all,

Some more thoughts about continuous assignments in checkers.

1. In the mail below I mentioned that the definition of a
continuous assignment in the Observed region requires a specific order
between checker variable assignments and execution of
assertions/assumptions/sequences. Strictly speaking this limitation is
not necessary. If it is not observed, the concurrent assertions may be
evaluated several times in the Observed region, but this should be
transparent to the user, since only the action block corresponding to
the last assertion evaluation will be executed in the Reactive region.
Of course, most implementers will prefer to order events appropriately
to boost the performance and to avoid pathological cases, but the event
ordering in the Observed region does not have to be mentioned in the
LRM, thus making the semantics of the continuous assignment of checker
variables similar to continuous assignments of other variables.

2. Sampling the RHS of a continuous assignment of checker
variables as suggested below makes deferred assertions second class
citizens in checkers: mixing checker and design variables in a deferred
assertion leads to assertion inconsistency. Workaround: explicitly
specify sampled values or use let instead of checker variables in
checker deferred assertions.

3. On the other hand the suggested definition makes introduction
of procedural and conditional operators in checkers smooth - all
conditions should be sampled (in the sense of the new definition)
regardless of the type of the procedure, even in always_comb.

What do you think?

Thanks,

Dmitry

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
Korchemny, Dmitry
Sent: Tuesday, November 16, 2010 2:30 PM
To: sv-ac@eda.org
Cc: sv-bc@eda.org
Subject: [sv-ac] Continuous assignments and checker variable sampling

Hi all,

I am copying SV-BC in case some SV-BC people want to take part in the
discussion. The below description has not been discussed yet in SV-AC.

It looks like we have a serious problem in the definition of continuous
assignments of checker variables. Consider the following example:

checker check (bit a, event clk);

                default clocking @clk; endclocking

                rand bit v;

                bit w, u;

                m1: assume property ($onehot0({a, v});

                assign w = !v;

                assign u = !a;

                a1: assert property ($onehot0({a, !w});

                a2: assert property ($onehot0({!u, v});

endchecker : check

It is natural to expect that assertions a1 and a2 always pass. The
question is whether checker variables w and u are sampled in the
Preponed region in concurrent assertions. If they are, assertion a1 will
fail. If they are not, assertion a2 will fail. This means that the RHS
of the continuous assignment should be sampled (i.e., regular variables
are sampled in the Preponed region, and the current value of free
variables is used), and that the continuously assigned checker variables
should not be sampled (in the Preponed region). This also means that the
continuous assignment should be performed in the Observed region, as was
suggested in the original version of the checker proposal (1900). This,
however, requires a refinement of the simulation semantics definition of
the Observed region by imposing some evaluation order in it. Some
ordering implicitly exists in the LRM at least since 2005. E.g., if a
sequence method is used in another sequence, the former sequence should
be evaluated before the latter one. LRM 2009 adds a new restriction that
free checker variables should be evaluated before the assertions where
they are used. Thus in the above example, the assumption m1 must be
evaluated before assertions a1 and a2. Introduction of the continuous
assignments requires imposing a stricter ordering: if variable x depends
on variable y then y should be evaluated before x. For the above example
it means that m1 is evaluated first, then the assignments in any order,
and then the assertions in any order.

There exists a strong objection against imposing any evaluation
ordering, but what is an alternative?

Thanks,

Dmitry

---------------------------------------------------------------------
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 <http://www.mailscanner.info/> , 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 <http://www.mailscanner.info/> , 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 <http://www.mailscanner.info/> , and is
believed to be clean. 
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.