Error reporting in OVL Assertions in Verilog.

Hi everyone,
In using Accellera assertions in Verilog, I have seen that for many
assertions, any error flagged is reported at the next clk edge (i.e.,
the active clk edge *after* the one where the error was detected). I
just want to know whether this behaviour is correct or not, because if
it's not, then I'm probably triggering the assertion incorrectly.

Could you please go through this very simple example of an
'assert_always' assertion ?

`define OVL_ASSERT_ON
`define OVL_INIT_MSG
`include "assert_always.vlib"

/*---- Module Definition ----*/
module ctr_4_bit (q, clk, clear);
output [3:0] q;
input clk, clear;
reg [3:0] q;
always @ (negedge clear or posedge clk)
begin
if (clear == 0) q <= 4'd0;
else q <= q + 1;
end
endmodule

/*--- Stimulus Block ----*/
module top;
reg clk, reset;
wire [3:0] q;
ctr_4_bit st (q, clk, reset);
initial
clk = 1'b0;
always
#1 clk = ~clk;
initial
begin
reset = 1'b0;
#1 reset = 1'b1;
#20 reset = 1'b0;
#1 $finish;
end

/*---- SHM Dump Block ----*/
initial
begin
$shm_open ("assert_always_example.shm");
$shm_probe ("as");
end

/*---- Assertion Block ---*/
assert_always #(
`OVL_ERROR,
`OVL_ASSERT,
"Error",
`OVL_COVER_ALL)

check (
clk == 1,
reset == 1,
q[2] == 1'b1);

endmodule

A very quick explanation: This program is a simple 4 bit counter and
it's allowed to run for a few clks and then made to end via the $finish
statement. The assertion has to flag the errors at all those clks where
q[2] = 1 doesn't hold true, right ?

The assertions are indeed triggering, but all of them are reported at
the consecutive clk of the error condition. For example, q[2] = 0 at
time = 1, 3 and 5 units in the output (I'm specifying only the posedges
of the clk) and the corresponding errors are reported at t = 3, 5 and 7
units. At t = 7, q[2] does become 1, and so, this should not set off
the assertion, but as I just mentioned, it does, which is what prompted
me to reach the conclusion that the bad behaviours may be reported 1
clk later.

Also, this particular property holds true for not only 'assert_always',
but many others, like 'assert_cycle_sequence', 'assert-handshake',
'assert_next', 'assert_no_overflow', 'assert_no_transition' etc.

If someone could tell me whether this is OK or not, I'd be really
grateful.

Thanks in advance,
Amit.

 

[Chris F Clark]

Yes, your assertions do (and should) happen one cycle later. The
"problem" is the non-blocking assignment. Note, you can model an OVL
assert_always with roughly the following code--the code in the library
isn't too far from this.

always @(posedge(clk == 1 /* what you specified for the clock */))
if (!(q[2] == 1 /* what you specified for the condition */))
$display("ASSERT");

So, on the posedge of the clk, it checks bit 2 of the signal q for
being 1.

Now, look at your other code, I've simplified it to:

always@(posedge(clk)) q<= q + 1;

That reads: on the posedge of the clk, calculate a new value of q and
schedule an update event to move it into q. That is the semantics of
a non-blocking assign, the value is moved, just a little bit later.
In particular, all checks of the value on the same edge happen before
the update and will see the "old value" of the signal being changed.
(The standard lays out in detail exactly the order the events should
happen in, including where the simulator can choose to do things in an
order of its choosing.) The only way to be certain that something
happens after the update of a non-blocking assign is to wait until the
target of the non-blocking assign changes. Therein lies the solution
to your problem.

You can get what you want, by just using the change in q[2] as your
clock. There isn't a requirement that the "clock" to an assert be a
clock of the model. It is just some signal that changes when you want
the check performed. Write an assert that is the equivalent of:

always @(posedge(!(q[2] == 1)))
if (!(q[2] == 1))....

Hope this helps,
-Chris

*****************************************************************************
Chris Clark Internet : compres@world.std.com
Compiler Resources, Inc. Web Site : http://world.std.com/~compres
23 Bailey Rd voice : (508) 435-5016
Berlin, MA 01503 USA fax : (978) 838-0263 (24 hours)
------------------------------------------------------------------------------

 

Hi Chris,
Many thanks for your help. There are some things though that I'm still
not clear on. Hope you won't mind clarifying them

I made some changes in the code as per your suggestions. These are as
follows:

Instead of the assert_width OVL assertion, I put your code (always @
(posedge clk == 1 /* ... which means no assertions altogether.

In the Module Definition, I removed the always @ (negedge clear ...
block and instead put what you suggested (always @ (posedge(clk))
q<=q+1; just before that I made q = 0 in an initial statement). This
effectively disables the reset control on the circuit.

After making these changes, I have seen that making the always @
(posedge(clk)) q <= q + 1; assignment blocking or non-blocking does not
make any difference and the outputs for both the cases are exactly
alike (next clk reporting). Outputs for q = q + 1; and q <= q + 1; are
the same.

I also used q[2] in place of clk for monitoring as suggested by you:
always @ (q[2]) /* monitor q[2] */
if (q[2] == 1) /* for a 1 */
$display ("%d ASSERT", $time);

In this case, the violations (a single one at t = 7 when q[2] goes high
for the first time) are reported at the *same* clk, and not at the
succeeding clk.

Now the question arises as to how does selecting a monitoring signal
(clk vs. q[2]) affect the error detecting/reporting behaviour.

Not using any assertions at all (and using simple always @ statements
to lookout for bad behaviour) and still getting next-cycle-flagged
errors makes me think whether this behaviour is a property of either
the language itself or the compiler/simulator that I am using.

Lastly, when you say that my assertions should happen 1 clk later, do
you mean in my specific implementation, or in the broad and general
sense (any assertion, any program) ?

Thanks once again.

Best regards,
Amit.

 

[Chris F Clark]

I will try to answer your questions.

After making these changes, I have seen that making the always @
(posedge(clk)) q <= q + 1; assignment blocking or non-blocking does not
make any difference and the outputs for both the cases are exactly
alike (next clk reporting). Outputs for q = q + 1; and q <= q + 1; are
the same.

This is not surprising. By changing to a blocking assignment, you
have introduced a race. There is no guarantee as to the order of
execution of two always blocks when one uses a blocking assignment and
the other inspects (reads, uses) a value. You may get the old value
or the new value. It may depend on the simulator you use, on other
code in your model, or even the "phase of the moon". It doesn't even
have to be consistent within one run of the model. It might give you
the old value one time and the new value another time. Therefore, if
you have a clocked always block, you should not use signals that you
assign in blocking assigns within that always block in another always
block.

In fact, there is no statement you can write the makes q change
"first" as part of the clock edge. You can use a non-blocking to make
q change "last", but blocking does not mean "first". That's not
really so bad, as real hardware works the same way. It always takes a
little while for the circuitry to react, so you can't really make
something happen instantaneously. Now, if you play around with clock
skew and buffers etc. you can slow parts of the chip down and you can
model that with #delays, but to my mind if you are doing that, you
aren't doing "digital" design naymore.

Not using any assertions at all (and using simple always @ statements
to lookout for bad behaviour) and still getting next-cycle-flagged
errors makes me think whether this behaviour is a property of either
the language itself or the compiler/simulator that I am using.

It is a property of the language. Any program with non-blocking
assignment statements will have the variables update sometime "after"
the clock but still in the same $time. The only reliable way to catch
the transition in the same $time is to wait on a transition of the
signal itself (or on some other signal that will depend on the
signal's transition). See the example below. With blocking assigns,
dues to races, the code may appear to work with some simulators at
some times, but isn't really correct.

always @posedge clock
a <= b;

always @posedge clock
c <= d;

always @posedge clock
$display( %time, "always old value: ", a );

always @a
$display( $time, "always new value: ", a );

assign e = a;

always @e // e depends on a
$display( $time, "always new value: ", a );

always @e // e depends on a
f = e;

always @f // f depends on e depends on a
$display( $time, "always new value: ", a );

always @f // f does not depend on c
$display( $time, "race: may display old or new value: ", c );

Hope this helps,
-Chris

*****************************************************************************
Chris Clark Internet : compres@world.std.com
Compiler Resources, Inc. Web Site : http://world.std.com/~compres
23 Bailey Rd voice : (508) 435-5016
Berlin, MA 01503 USA fax : (978) 838-0263 (24 hours)
------------------------------------------------------------------------------

 

Hi Chris,
Thanks again for your reply and clarification. It did help to clear
many of my doubts.

Best regards,
Amit.