Concurrent Assertion :: Capturing time in different context

SystemVerilog
,
1

Hi all ,

The following is an example given in SV LRM Section 16.6 ::


bit [2:0] count;
realtime t;
initial count = 0;

always @(posedge clk) begin
if (count == 0) t = $realtime; //capture t in a procedural context
count++;
end

property p1;
@(posedge clk) count == 7 |-> $realtime – t < 50.5;
endproperty

The LRM says :: " The comparison between values of time captured in the different contexts yields an inconsistent result"

However I am not sure what the issue is . Why won’t the above logic work ?

The LRM suggests to use ::


property p2;
realtime l_t;
@(posedge clk)
(count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime – l_t < 50.5;
endproperty
2

In reply to hisingh:
The point of 1800:16.6 Boolean expressions is that “Assertions that perform checks based on time values should capture these values in the same context. It is not recommended to capture time outside of the assertion. Time should be captured within the assertion using local variables”. The main issue is that assertions use sampling values in the Preponed Region, whereas values within the always @(posedge clk) are in the Active region and may not be the same as the sampled values.
I modeled this example as shown in Edit code - EDA Playground
and I did not see any assertion errors. However, I still stand by what the point made in 16.6.

A general guideline for SystemVerilog is to always stick to strict coding rules so that the simulation emulates concurrency per the modeling of the evaluation regions:

  • For assertions, use sampled values for signals. Any timing measurements should be related to sampled values of signals.
  • Clocked signals should be updated using the nonblocking <= operator
  • Never mix blocking and nonblocking assignments to signals (except for initialization.

One critique on the bad modeling style addressed is that the assertion
@(posedge clk) count == 7 |-> $realtime – t < 50.5;
evaluates in ONE cycle, though it checks 2 events that occur at different times. Those events are count==0 and count==7. That p1 assertion lacks that depth of definition because the “t” was defined somewhere else.
However, p2 clearly clarifies the requirements:
(count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime – l_t < 50.5;

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

3

In reply to hisingh:
Thee is an error in 1800. Change in 16.6 Boolean expressions
FROM:


always @(posedge clk) begin
   if (count == 0) t = $realtime; //capture t in a procedural context
   count++;
end

TO:


always @(posedge clk) begin
   count++;
   if (count == 0) t = $realtime; //capture t in a procedural context
end