Hi Manisha:
You wrote:
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
In this example for sanity1 to pass, the cont assign to w should happen
before asserts are executed. And at the same time, for sanity2 to pass,
cont assign to b should happen after asserts are executed (as cont
assign uses current value of RHS but assertion uses sampled value).
The LRM says the following about continuous assignments in 10.3.2:
Assignments on nets or variables shall be continuous and automatic. In
other words, whenever an operand in
the right-hand expression changes value, the whole right-hand side shall
be evaluated. If the new value is
different from the previous value, then the new value shall be assigned
to the left-hand side.
I think that we should try to follow this model if possible.
I think that "assign b = a;" is going to have to be performed in
response to a change in "a". In whatever time step "a" changes, I
think that an update to "b" needs to occur in that time step and after
the change to "a". I think that checker continuous assignments should
always evaluate their RHSs with current values. So I think that "assign
b = a;" should cause the preponed values of "a" and "b" to be the same
in any time step (the very first time step being a possible exception),
and therefore I believe that sanity2 will always pass (the very first
time step being a possible exception).
Similarly, I think that "assign w = v;" should be performed in response
to a change in "v". "w" should be updated in the same time step to have
a value matching that of "v", and so I believe that sanity1 will always
pass (the very first time step being a possible exception).
Since the preponed values of "a" and "b" are the same and the preponed
values of "v" and "w" are the same, a1 and a2 should always either both
pass or both fail (the very first time step being a possible exception).
"v" will only change in a time step in which m1 is solved. My thinking
is that m1 needs to be solved using current values and in response to a
change in "a". If m1 is solved in the same time step that "a" changes,
then we will always have the $onehot(a, v) holds for preponed values of
"a" and "v" (the very first time step being a possible exception).
More generally, solving of m1 could be done after "a" changes and
strictly before the next time step in which clk occurs. Again, if m1
is solved using the current value of "a", then $onehot(a,v) will hold
for preponed values of "a" and "v" in time steps at which clk occurs
(the very first time step being a possible exception).
As long as $onehot(a,v) holds for preponed values in time steps in which
clk occurs, a1 and a2 will both pass, and m1 will pass when evaluated as
a checker using preponed values.
The trick in this approach seems to be figuring out when to solve m1 for
"v" to make sure that $onehot(a,v) holds for preponed values in every
time step in which clk occurs. Solving in response to change in "a"
seems to work.
Best regards,
John H.
I believe that m1 should be solved in every time step in which clk
occurs.
From: Kulshrestha, Manisha [mailto:Manisha_Kulshrestha@mentor.com]
Sent: Thursday, November 25, 2010 10:13 PM
To: Havlicek John-R8AAAU; Eduard Cerny; Korchemny, Dmitry; sv-ac@eda.org
Cc: Little Scott-B11206
Subject: RE: [sv-ac] RE: Continuous assignments and checker variable
sampling
Hi,
Lets take this original example:
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
In this example for sanity1 to pass, the cont assign to w should happen
before asserts are executed. And at the same time, for sanity2 to pass,
cont assign to b should happen after asserts are executed (as cont
assign uses current value of RHS but assertion uses sampled value).
Now, lets look at what currently exists in the LRM:
checker check (bit a, event clk);
default clocking @clk; endclocking
rand bit v;
bit w;
bit b;
m1: assume property ($onehot0({a, v});
a1: assert property ($onehot0({a, v});
always @(clk)
w <= v; // uses sampled value of RHS
always @(clk)
b <= a; // uses sampled value of RHS
sanity1: assert property (w == v);
sanity2: assert property (b == a);
endchecker : check
In this example also sanity2 can not hold as b is assigned sampled value
of a after asserts have been evaluated. Similarly, sanity1 will not hold
either as assert is executed before w gets its value based on v.
So, looks like this problem of mixing different types of vars with
design variables in assertion has been there.
Manisha
________________________________
From: Havlicek John-R8AAAU [mailto:r8aaau@freescale.com]
Sent: Thursday, November 25, 2010 10:16 PM
To: Eduard Cerny; 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 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, and is believed to be clean.Received on Fri Nov 26 12:30:52 2010
This archive was generated by hypermail 2.1.8 : Fri Nov 26 2010 - 12:33:56 PST