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

Hi,

I so far do not see a solution, it seems that one way or the other, there is some issue. There is one invariant, however, that should hold no matter what solution we take. If there is an assumption and an assertion of the same form, location and content, the assertion must always pass. Would you agree?

ed

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

Hi Dmitry:

I agree that if the sampled values of other variables are used when solving for free variables, then you will have a mess.

J.H.

From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]
Sent: Tuesday, November 23, 2010 8:13 AM
To: Havlicek John-R8AAAU; Kulshrestha, Manisha; sv-ac@eda.org
Cc: Little Scott-B11206
Subject: RE: [sv-ac] RE: Continuous assignments and checker variable sampling

Hi John,

I understood from Manisha's proposal that free variables are resolved according sampled values of other variables.

Thanks,
Dmitry

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

Hi Dmitry:

I disagree.

If the free variable "b" is solved using the current value of "a" in m1, then a1 will not fail provided "b" is solved after "a" is updated. It doesn't matter whether "b" is solved in Observed or in Reactive (or later).

J.H.

From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]
Sent: Thursday, November 18, 2010 10:27 AM
To: Kulshrestha, Manisha; Havlicek John-R8AAAU; sv-ac@eda.org
Cc: Little Scott-B11206
Subject: RE: [sv-ac] RE: Continuous assignments and checker variable sampling

Hi Manisha,

Consider the following example:

checker check (bit a, event clk); // a is a design variable
                rand bit b;
                m1: assume property (@clk a == b);
                a1: assert property (@clk a == b);
endchecker

It is natural to expect that the assertion a1 always passes. However, if free variables are updated in the Reactive region, a1 will fail. Am I correct?

Thanks,
Dmitry

From: Kulshrestha, Manisha [mailto:Manisha_Kulshrestha@mentor.com]
Sent: Thursday, November 18, 2010 11:48 AM
To: Korchemny, Dmitry; Havlicek John-R8AAAU; sv-ac@eda.org
Cc: Little Scott-B11206
Subject: RE: [sv-ac] RE: Continuous assignments and checker variable sampling

Hi Dimitry,

 There is another alternative. We can update the free checker variables in Reactive region (instead of Observed region) and assertions would use previous values of free checker variables. So, assumptions would be evaluated in Observered region but their effect on the free checker variables would be visible in reactive region. Even deferred assertions would work fine in this case even if we mix checker variables and design variables in them. Also, the continuous assigns will also update values in Reactive region.

Since non-free checker variables are updated in Re-NBA region, having all the things in checkers update in Reactive region small loop (Reactive, Re-Inactive, Pre-Re-NBA, Re-NBA, Post-Re-NBA) would be consistent.

Manisha

________________________________
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Korchemny, Dmitry
Sent: Thursday, November 18, 2010 1:11 PM
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.
---------------------------------------------------------------------
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.
---------------------------------------------------------------------
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.