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

Hi John,

Actually we did discuss similar proposals at the face-to-face meeting
where we eventually decided on the implementation of free checker variables.

One proposal was to solve for free variable values at the very beginning
of the time-step (in Preponed or just after). The problem with this
proposal was that we didn't want to be solving for free variable values
in every time-step, but only in time-steps where clocking events
occurred. But, you don't know if a clocking event will occur until the
end of the Active or NBA region!

Another proposal was to solve for free variable values at the end of the
time-step (just before Postponed) using actual values. This, I think
is very similar to the idea you are proposing. The theory was that the
final values computed in the time-step would be the sampled values in
the time-step where the next clocking event occurred. This would work
in a totally synchronous design, but if there are asynchronous signals,
or even pound-delay assignments, then signals could change values, and
as a result, the chosen free variable values might not meet the
constraints when simulation reaches the time-step where the next
clocking event occurs.

The result was, the only possible place we could solve for free variable
values was at the beginning of the Observed region. It's not very
pretty, but I don't think there is sufficient reason to change it, just
to make continuous assignments in checkers work.

Tom

On 11/25/10 08:46, Havlicek John-R8AAAU wrote:
> Hi Ed:
>
>
>
> I think your statement is a goodness criterion that should only be
> broken for very good reasons.
>
>
>
> My general understanding is that we need to solve for free variables
> using current values of non-free variables. Otherwise, we have timing
> issues and your goodness criterion will not hold. Further, we need to
> solve for free variables after the non-free variables have done there
> changing. In general, we cannot do this is if the solving is unable to
> predict when other variables change or is unable to react to the changes
> of other variables. So there may be some cases when we cannot achieve
> the goodness criterion due to infeasibility of coordination of the
> solving with changes of various variables.
>
>
>
> Continuous assignment in checkers is another question, but I think it
> also has an important goodness criterion: If we write
>
>
>
> assign foo = bar;
>
>
>
> then we should expect
>
>
>
> assert property (foo == bar);
>
>
>
> to hold (assuming that foo and bar have the same type).
>
>
>
> I recommend writing down simple examples that illustrate the interplay
> between free variables, non-free variables, and continuously assigned
> variables, where various entities are updated in reactive, observed,
> reactive, etc. and trying to distill the common theme. This is the
> direction that Scott and I were heading that lead us to the rules we
> proposed below. Another example to consider is a free variable
> interplaying with a local variable. I think that this approach will
> help us to achieve the goodness criteria in most cases of interest and
> to understand why we need to sacrifice the goodness criteria in some
> cases if necessary.
>
>
>
> J.H.
>
>
>
> *From:* Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]
> *Sent:* Thursday, November 25, 2010 10:35 AM
> *To:* Havlicek John-R8AAAU; Korchemny, Dmitry; Kulshrestha, Manisha;
> sv-ac@eda.org
> *Cc:* Little Scott-B11206
> *Subject:* 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* <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.