Date: Thu Dec 02 2010 - 13:02:09 PST
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
<http://www.twitter.com/dave_59> <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. 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, and is believed to be clean.
