Tuesday, 20 May 2014

How to Write Action blocks in Assertions

Usual tendency is to write display statements in action blocks(report blocks) to display the error and values. since, the way assertions are executed is a bit different, please go through below example to understand how to write action blocks using $sampled.
***********************************************************************************
This quiz shows a subtle "gotcha" with SystemVerilog Assertions.  The example comes from a real problem encountered at a commpany, though the code has been simplified to focus on the "gotcha" in the assertion.
The assertion verifies that the value of a parity bit is set correctly for the value of data for every clock cycle.  An assertion failure indicates something is wrong with either data or the parity generator logic. 
Assertion Code
property p_parity_check;
  @(posedge clk)
  disable iff (!rstN)  // no checking during active-low reset
  parity == ^data;
endproperty

pcheck: assert property (p_parity_check)
else $error("PARITY ERROR at %0d ns: data = %h, even parity = %b (expected %b)\n",
            $realtime, data, parity, ^data);
This assertion has a subtle "gotcha" when there is an assertion failure.  To illustrate the problem, the design under test for this example always generates a 1 for the parity, which is occasionally an incorrect parity value.  The assertion appears to work most of the time, but sometimes reports an error even though the values printed out in the error message indicate that the data and parity values are correct.  In the following simulation output, the first assertion failure is a real failure, but the second error seems to be incorrect — the value of parity is the right value for the value of data.
Simulation Output
# At 15: Requesting data
# ** Error: PARITY ERROR at 15 ns: data = 00, even parity = 1 (expected 0)
# ** Error: PARITY ERROR at 25 ns: data = 01, even parity = 1 (expected 1)
# At 45: Requesting data
# At 75: Requesting data
Waveform
pcheck             P    F    F    P    P    P    P    P

         +----+    +----+    +----+    +----+    +----+
clk      |    |    |    |    |    |    |    |    |    |
     ----+    +----+    +----+    +----+    +----+    +----

     +        +--------------------------------------------
RSTn |        |
     +--------+

     ------------------------+-------------------+---------
data    00 (hex)             | 01 (hex)          | 02 (hex)
     ------------------------+-------------------+---------

              +--------------------------------------------
parity        |
     ---------+
Why did the assertion show a second failure when the printed values are correct at that time?
Answer
The "gotcha" in this assertion has to do with the order in which simulators evaluate assertions, print messages, and change design signal values.  The IEEE SystemVerilog defines a specific order for processing events on a clock edge.
  1. Any signals to be evaluated by a concurrent assertion are "sampled" in a "Preponed event region" of a clock edge.  This is a stable point, before any signal changes that might occur as a result of the clock edge have been processed.
  2. Next, design modules process signal changes in the "Active event region" and the "NBA Update event region".
  3. After the design changes for that clock edge are processed, assertions error messages are printed in a "Reactive event region".
This delta between sampling values and the assertion results from processing those values represents register-based hardware clock-to-Q behavior, and is as it should be.  It does mean, however, that, by the time the pass/fail statements are executed, RTL code can, and probably will, be changing signal values due to the clock edge.
In the assertion in the example above, it appears that the second failure message should not have happened -- the value or parity appears to be correct, and yet the assertion failed.  The real problem, though, is that the assertion error message is showing the value of data after the assertion has sampled data.  The sampled value wass not the same as the printed value.  The assertion failure was correct, but the error message was misleading.  Gotcha!.
SVA has a simple solution for this "gotcha".  If a pass/fail statement needs to print the values of signals that are used by the assertion, then the message should print the Preponed value — the same value used by the assertion — by using the $sampled() function.  $sampled() returns the Preponed value of a signal for the current moment in simulation time.  the correctly written assertion for this example is:
property p_parity_check;
  @(posedge clk)
  disable iff (!rstN)  // no checking during active-low reset
  parity == ^data;
endproperty

pcheck: assert property (p_parity_check)
else $error("PARITY ERROR at %0d ns: data = %h, even parity = %b (expected %b)\n",
            $realtime, $sampled(data), $sampled(parity), ^($sampled(data))); 
 
******************************************************************************************** 

No comments:

Post a Comment