SVA for delayed state transition from FAULT_ID to WAIT_STATE (100ms delay)

SystemVerilog
1

Hi,

I want to write an assertion for the following requirement:
From state: FAULT_ID
To state : WAIT_STATE
Condition : The transition should happen only after 100ms delay

Here’s the assertion I tried:

property ppt;
  time t1;
  @(posedge clk) disable iff(!rst_n)
    $changed(cur_st) && (cur_st==FAULT_SD, t1=$time)
    |=> cur_st==FAULT_SD until (($time-t1)*1000000 == 100ms) ##0 cur_st==WAIT_LDO1_POK;
endproperty : ppt

I heard that this kind of check can also be achieved using first_match constructs.
Is my approach correct?
Would first_match be a better option here?
Any recommended clean way to model this delay-based state transition?

Thanks in advance!

2

I would have written the property as

property ppt;
      realtime t1;
      @(posedge clk) 
        ($rose(cur_st==FAULT), t1=$realtime) |=>
     cur_st==FAULT [*] ##1 cur_st==WAIT ##0 $realtime-t1 > 100ms
endproperty : ppt

There’s no need for first_match() here as you have only one variable involving simple boolean sequences.

Scaling $time* 1000000 is a mistake. 100ms gets scaled to the local timescale.

Timing checks should be performed using realtime and relational operators instead of equality. Achieving exact equality becomes extremely challenging due to the fact that getting the clock period precisely and accounting for rounding errors make it very difficult.

3

Is it a good idea to use $(real)time inside a property? Would it perhaps be better to count clock edges to check the condition in this case? What if the time of the state change differs due to clock variation?

4

It really depends on the source of the requirements. However, if you want to formally verify this assertion rather than through simulation, clock cycles would be a more appropriate.

1 Like