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

Scott,

Let me see if I understand your proposal.

You are thinking that the solving process would be triggered not just by
the clocking events of the assume property statements, but also by
changes to signals/variables referenced by those assume property
statements. The solving uses current values, and essentially solves for
the value of the free checker variable that will be used by the
assertions when the next clocking event occurs.

When the next clocking event does occur, the free variables would be
sampled, like any other signal, and the assume property statements would
be evaluated like any other assertion. If the solver failed to find a
solution, one of the assume property statement could fail.

I think that this is a very elegant solution. If we put the solving
somewhere in the Reactive region set, then everything within the checker
would be updating consistently. And the Observed region would go back
to being strictly for checking assertions.

Another benefit is that free variables would "look right" when displayed
in a waveform. Currently, assertions use the sampled values of signals,
whereas they use the current values of the free variables. If displayed
  on a waveform today, the free variable value just after the clocking
event corresponds to the signal values that occurred just before the
clocking event.

The only concern I have is whether the current problems are serious
enough to warrant the change. Currently, the only reason we are
proposing this is to enable the addition of continuous assignments.

Tom

On 12/02/10 13:02, Little Scott-B11206 wrote:
> On a reread this may not be totally clear. My thought would be to
> associate the solving event control with the assume statements in a
> similar way to how checking event control is specified. This would mean
> that assume statements in checkers would have a solving event control as
> well as a checking event control. It is likely they would be different.
>
>
>
> Thanks,
>
> Scott
>
>
>
> *From:* Little Scott-B11206
> *Sent:* Thursday, December 02, 2010 2:58 PM
> *To:* Korchemny, Dmitry; Rich, Dave; sv-ac@eda.org
> *Subject:* RE: [sv-ac] RE: Continuous assignments and checker variable
> sampling
>
>
>
> Hi Dmitry:
>
>
>
> I believe I understand your concern. One idea I had to potentially
> address this is to allow event control on the free variables that
> determines when they are solved. For instance, let’s say that changes
> to design and TB variables happen on the posedge of clk. Then couldn’t
> we solve the free variables on the negedge of clock or even an event
> that is generated #1step after posedge clk? I guess this means that the
> solving of a constraint would be triggered at the nearest specified
> event control after a change in the assume set clock event.
>
>
>
> The main idea here is to solve for the constraints at a time when you
> are confident both the design and TB signals have been updated. We
> don’t have a point in the simulation cycle where this is true. We
> should be able to specify a different cycle where this is true and just
> solve in that cycle. What do you think about that?
>
>
>
> Thanks,
>
> Scott
>
>
>
> *From:* Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]
> *Sent:* Thursday, December 02, 2010 12:37 PM
> *To:* Rich, Dave; Little Scott-B11206; sv-ac@eda.org
> *Subject:* RE: [sv-ac] RE: Continuous assignments and checker variable
> sampling
>
>
>
> Hi Dave,
>
>
>
> Here is a definition proposed by John and Scott:
>
>
>
> 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.
>
>
>
> and a clarification:
>
>
>
> 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.
>
>
>
> My question is: what happens if the expression which is an actual
> argument for a is updated in the Reactive region? This is what I call a
> “TB variable”. My concern that in this case the simulation semantics is
> not well defined (though I may be wrong).
>
>
>
> Thanks,
>
> Dmitry
>
>
>
> *From:* Rich, Dave [mailto:Dave_Rich@mentor.com]
> *Sent:* Thursday, December 02, 2010 8:30 PM
> *To:* Korchemny, Dmitry; Little Scott-B11206; sv-ac@eda.org
> *Subject:* RE: [sv-ac] RE: Continuous assignments and checker variable
> sampling
>
>
>
> Dmitry,
>
>
>
> Yes, I understand this is a working discussion. I’m just trying to make
> sure things don’t get out out of hand. Adding more regions is not the
> way to go.
>
>
>
> Some questions:
>
>
>
> What is your deffintion of a TB variable, and why do you think it would
> be updated in the reactive region?
>
>
>
> Dave
>
>
>
> *From:* Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]
> *Sent:* Thursday, December 02, 2010 9:34 AM
> *To:* Rich, Dave; Little Scott-B11206; sv-ac@eda.org
> *Subject:* RE: [sv-ac] RE: Continuous assignments and checker variable
> sampling
>
>
>
> Hi Dave,
>
>
>
> This is just a working discussion. There were several proposals
> suggested to define continuous assignment of checker variables and we
> are trying to understand the implications of each of them. In this
> specific case the proposed solution requires according to my
> understanding solving free variables at the very end of a simulation
> tick, somewhere like the Postponed region. This cannot be the Postponed
> region, though, because it is forbidden to change variable values there.
> This is what I meant under an additional region after the reactive
> region set. This is not similar to a re-reactive region.
>
>
>
> Do not consider this as the SV-AC proposal unless SV-AC decides that
> this is the direction to go. If this will be the case, we will summarize
> the proposal and send it to SV-BC for review.
>
>
>
> Thanks,
>
> Dmitry
>
>
>
> *From:* Rich, Dave [mailto:Dave_Rich@mentor.com]
> *Sent:* Thursday, December 02, 2010 6:06 PM
> *To:* Korchemny, Dmitry; Little Scott-B11206; sv-ac@eda.org
> *Subject:* RE: [sv-ac] RE: Continuous assignments and checker variable
> sampling
>
>
>
>
>
>
>
> Dave Rich
> Verification Technologist
> Mentor Graphics Corporation
> *New Office Number: 510-354-7439*
>
> *Twitter-32* <http://www.twitter.com/dave_59>*Technorati-32*
> <http://go.mentor.com/drich>
>
>
>
>
>
> Assuming resolve the free variables is equivalent to solving for the
> free variables, you say we would have to change the global simulation
> scheme to achieve this. I don’t quite understand. The LRM states:
> “When an implementation is about to begin the Observed region, it shall
> solve for all the active free variables.” Aren’t free variables already
> solved in the Observed region?
>
>
>
> */[Korchemny, Dmitry] Consider the following assumption: assume property
> (v == a); where v is a free variable, and a is a TB variable, which is
> updated in the Reactive region. You have to check your assumption in the
> Observed region with the preponed values of v and a, and then to solve v
> in the Reactive zone to get the new value of v. It turns out that you
> process your assumption twice in the simulation tick. Essentially, the
> situation is even worse, since you have to solve your assumption each
> time when a changes to be sure that the value of v is always updated.
> This is very expensive. The alternative is to introduce an additional
> region that executes after the reactive region zone. /*
>
> */[DR] Please do not even think of that alternative. The alternative is
> not use the reactive region. Please see /*go.mentor.com/programblocks
> <http://go.mentor.com/programblocks>. */The/* */whole point of the
> re-active region was so that it wouldn’t modify the DUT or the
> assertions for the current time step. But if you must include TB
> variables updated in the reactive region in assertions, you could have
> a restriction that says that variable must not be updated in the current
> time step. That might be a difficult rule to enforce./*
>
>
>
>
>
> *From:* Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]
> *Sent:* Tuesday, November 23, 2010 8:11 AM
> *To:* Havlicek John-R8AAAU; sv-ac@eda.org
> *Cc:* Little Scott-B11206
> *Subject:* RE: Continuous assignments and checker variable sampling
>
>
>
> Hi John,
>
>
>
> Unless you modify the global simulation scheme and resolve the free
> variable in the Observed region, the following example won’t work:
>
>
>
> rand bit v;
>
> assume property (@clk v == a); // a is updated in the Reactive region
>
>
>
> The value of v will never be updated. If you evaluate assumptions using
> sampled values of free variables and then resolve free variables in
> assumptions using current values of all variables, you will have to
> evaluate the assumptions twice. I think you need to explicitly state the
> details of your proposal. Let’s discuss it today if time permits.
>
>
>
> Thanks,
>
> Dmitry
>
>
>
>
>
> *From:* Havlicek John-R8AAAU [mailto:r8aaau@freescale.com]
> *Sent:* Thursday, November 18, 2010 6:41 PM
> *To:* Korchemny, Dmitry; sv-ac@eda.org
> *Cc:* Little Scott-B11206; Havlicek John-R8AAAU
> *Subject:* 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:
>
>
>
> 4. Checker continuous assignments should use current values of
> their righthand sides and happen after solving for checker free variables.
>
> 5. Checker free variables should be solved using current values of
> the non-free variables.
>
> 6. 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.
>
> ---------------------------------------------------------------------
> 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.