Assertion to check delay between two signals

SystemVerilog
,
1

I wanted to write an assertiion such that the delay between the “a” rise to “b” rise should be 2.1ns.
Written below code, buts it is not working. Any idea?

property a_to_b_rise(a, b);
    realtime a_rose;
  @(posedge clk) disable iff (!rst_n)
  ($rose(a), a_rose = $realtime) |-> ##[0:$] ($rose(b) && (($realtime - a_rose) > 2.1)); 
endproperty
2

In reply to satyendrasoni05:
A few things:

  1. What do you mean by “it is not working” ? Do you see a compilation error or assertion failure or do you mean the assertion isn’t working as per intention
  2. What are the timeunits and timeprecison in the module/checker where these assertions are written ?
  3. What are the units and precision of the module where the clock is generated ?

Note that $realtime returns a real value scaled to the timeunits of the module/checker where the assertion is written.

So if the units of the clock generator are different than the units of the assertion,
the value returned by $realtime could be different than expectation.

3

In reply to Have_A_Doubt:

  1. Compile is fine, but assertion is not failing as intended. Basically when “a” rise and “b” rise is at same clock. Assertion should fail as the delay between them will be 0.

  2. timeunit is ns with precision is ps;

I am using EDA playgroud to run the assertion. So timeunit/precicion problem will not be there as have single module.

4

In reply to satyendrasoni05:

Please share the edalink

5

In reply to Have_A_Doubt:

6

In reply to satyendrasoni05:

I observe that in the edalink within the consequent you have written ‘i_gpio’ instead of ‘$rose(i_gpio)’

The reason why the assertion doesn’t fail is it’s waiting for sequence: ( $rose(i_gpio) ) && (($realtime - oe_rose) > 2ns)) to occur/match .

In your case the sequence doesn’t match since: (($realtime - oe_rose) > 2ns) isn’t true.

Based on the intention the assertion should be written as:


property oe_to_i_gpio_rise(gpio_oe, i_gpio);
    realtime oe_rose;
  @(posedge clk_rmii_i) disable iff (!rst_n)
  ($rose(gpio_oe), oe_rose = $realtime) |->  $rose(i_gpio)[->1]  ##0 (($realtime - oe_rose) > 2ns); 
endproperty
7

In reply to Have_A_Doubt:

Agree, **( $rose(i_gpio) ) && ((realtime - oe_rose) > 2ns))** will never will true as ##[0:] is not correct usage.

Can you please elaborate “$rose(i_gpio)[->1]” ?

8

In reply to satyendrasoni05:

Using the go-to repetition operator [->1] via $rose(i_gpio)[->1] it essentially waits for the 1st occurrence of $rose(i_gpio).
Due to overlapping implication , $rose(i_gpio) is checked from same clock tick when the antecedent is true.

9

In reply to satyendrasoni05:

Got it. So $rose(i_gpio)[->1] basically means on the last cycle when $rose becomes true. !rose(i_gpio)[*0:] ##1 $rose.

Thanks

10

In reply to satyendrasoni05:

In the consequent I was trying to use ##[0:$] $rose(b) as an alternative to $rose(b)[->1] ,
here is the link for differences between the two.