Subject: [sv-ac] False firing of assertions examples.
From: Adam Krolnik (krolnik@lsil.com)
Date: Wed Sep 04 2002 - 16:23:47 PDT
Good afternoon all;
Here is an example of a false firing of an assertion in a
combinatorial block.
The heart of the example looks like this:
always @(s1 or s2 or d1 or d2)
begin
...
// We can't have s1 and s2 on otherwise we give bad data.
if (s1) assert (! s2);
do = s1 & d1 | s2 & d2;
end
If you ran this on your favorite SystemVerilog simulator, there
may be a possibility of this assert statement reporting an error
that is false.
Here we see the output of $monitor and the assertion error message.
0 s1 = 0, s2=0
10 s1 = 1, s2=0
Error at time 20 - s1 and s2 are true.
20 s1 = 0, s2=1
30 s1 = 0, s2=0
$finish at simulation time 80
But wait, time 20 does not show the selects (s1, s2) in that state -
whoa!!
This is due to intra-timestep value changes inherent in the simulator.
Okay, how do we fix this?
[ Don't use procedural assertions - use declarative!]
On a lighter note there is a way to trade this problem for another,
but this other problem is an annoyance to designers.
We need to add this statement:
disable checkit;
This statement will disable the assertion if it was started due to
a previous value change (either in the same timestep or a previous
step.) This will prevent an assertion from firing if the antecedent
path (in our case, s1) changes value such that the assertion is no
longer going to be evaluated. A designer will need to add a disable
statement for each assertion that they write in a combinatorial
block. Failure to add this mandatory disable may result in a false
failure of the assertion.
In addition to this extra statement (at the beginning of the block)
the designer will need to use assert_strobe instead of an immediate
assertion. This is because the immediate assertion would have already
generated the error message. Use of the strobed assertion will delay
the evaluation of the assertion until we know the values are stable.
Thus our simple example is now (more complex):
always @(s1 or s2 or d1 or d2)
begin
disable checkit; // disable the assertion ??!! :(
...
// We can't have s1 and s2 on otherwise we give bad data.
if (s1) checkit: assert_strobe (! s2);
// Our functionality that we are preventing.
do = s1 & d1 | s2 & d2;
end
Thus, we should now recommend the following:
1. Use a disable statement FOR EACH assertion in a combinatorial
block. Make sure you name your assertion too! This disable
shall be placed at the beginning of the block.
2. Use a named (always) assert_strobe statement in combinatorial
blocks to allow prevention of false firings.
Okay great...
Let's hook this up to some other code we have here....
Okay, let's run it...
0 s1 = 0, s2=0
10 s1 = 1, s2=0
Error(2) at time 20 - s1 and s2 are true.
20 s1 = 1, s2=1
21 s1 = 0, s2=1
30 s1 = 0, s2=0
$finish at simulation time 80
Hey -- what's the deal!!!! I get an error at time 20 and the $monitor
says the selects are both on - this must be real...
Wait!! At time 21 (#1 later), the selects are okay - argggh!
My other code has a different coding style and it uses # delays,
or the IO's have some gate delays within them...
Okay, now we have inter-timestep delays that must be accounted for in
our assertion methodology...
Okay, let's modify our assertion a little bit more to this somewhat
strange form.
always @(s1 or s2 or d1 or d2)
begin
disable checkit; // Methodology recommendation #1
// We can't have s1 and s2 on otherwise we give bad data.
// Check s2 at the end of the cycle - before the registers update to
// their new values. Wierd - yes!
if (s1) checkit: assert (1;!s2) @@(posedge clk);
// Our functionality that we are preventing.
do = s1 & d1 | s2 & d2;
end
So we use the disable (to disable previously evaluated assertions), then
we use a immediate assert statement?! Wait that violates methodology #2.
Okay, so what - does it work? YES! But it's wierd, I have to now check
my expressions in the next timestep (but before the new values arrive?!)
Ohhhh, is this going to work? Yes it should...
Alright, what's our methodology.
1. Use a disable statement FOR EACH assertion in a combinatorial
block. Make sure you name your assertion too! This disable
shall be placed at the beginning of the block.
2. Always use the form "<name>: assert (1;<expr>) @@(posedge clk)"
statement in combinatorial blocks to allow prevention of
false firings.
One caution is this note in the SystemVerilog 3.0 draft (pg 46)
"Note that to avoid races, the variables read in clocked immediate
assertions
should be written by nonblocking assignments."
This conflicts with out proposed methodology, we'll have to see what
should
happen.
This is for combinatorial blocks - for sequential blocks, what should we
do.
3. For sequential blocks, one may use immediate assertion statements
to check for correct values. Since the assertion is executed in a
sequential block, there will be no unstable signal values.
The only drawback to use of the immediate assertions is that they are
evaluating the signals "at the end of the cycle". By this I mean that
the signals will receive a new value at the end of the current timestep
(through nonblocking, continuous assignment or procedural assignments.)
An error message will report this current time as the time of faiure.
Debugging tools will show the new signal values at this time, causing
a little bit of confusion. One will have to step back to the previous
cycle to see the (in)correct values to debug from.
I am including 4 attachments that show these examples. They are:
intra.v - example with intra-timestep problems.
inter.v - example with inter-timestep problems.
intra.sv - system verilog version (hopefully)
inter.sv - system verilog version
You can see (not see) the problem by running these on your simulator
and including the +define statements listed in the file to prevent
the problems.
Maybe we should consider extracting procedural assertions and their
context and simulating them as declarative assertions.
Thanks.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Wed Sep 04 2002 - 16:26:55 PDT