Detecting live-lock using SV assertion

SystemVerilog
,
1

Hi,

Live-lock is when two states of a SM keep bouncing between each other in perpetuity. For example, S1 transitions to S2 and S2 transitions to S1. And this keeps going on forever prohibiting state machine to advance.

From SV assertion point of view, I’m trying to write an assertion when on detection of such bouncing states (for, let’s say 32 transitions), the assertion fails.

I know how to write an assertion for a dead-lock but not sure how to write an assertion for live-lock.

Any ideas?

Thanks much.

2

In reply to a72:
Is this what you are looking for?


bit lk;
function void set_lk(bit x);
  lk=x;
endfunction 

assert property(@ (posedge clk) 
  (st==S1 && !lk, set_lk(1)) |-> 
     not((st==S1 ##1 st==S2) [*32])) 
           set_lk(0); else     set_lk(0));

Ben systemverilog.us

3

In reply to ben@SystemVerilog.us:

Thanks but I am not sure, I fully understand the use of set_1k.

4

In reply to a72:

But the following core assertion should work.

not((st==S1 ##1 st==S2) [*32]))

thanks.

5

In reply to a72:

not((st==S1 ##1 st==S2) [*32])) should work.

I was not clear on the requirements. I used the set_1k to exclude
other st==S1 from refiring until the triggered assertion passes or fail.
But on 2nd thoughts, you don’t need it.
Ben systemverilog.us

6

In reply to ben@SystemVerilog.us:

Thanks, Ben.