Check Assertion for FSM state with unknow number of cycles before state change

SystemVerilog
, , ,
1

I have a FSM in which the State is Changing from A to B and there are let say (1510 clock cycles) between them. How do i write the assertion to check if the transition is happening from State A to State B. At state A a counter start (C) which goes till 1FFF(corresponding to 1510) and at that point signal ‘done’ gets high. With this information how do i write the Assertion ? i DO NOT want to mention number of cycles in the assertion unlike what i have done in the example below.

property p_FSM_A_B;
@(posedge clk) disable iff (!rst)
(state==A) ##1510 done |=> (state==B, $display(" A - B")) ;
endproperty : p_FSM_A_B

ap_FSM_A_B: assert property (p_FSM_A_B) else
      $error("Fail");
2

In reply to pagarwa5:


property p_FSM_A_B_option1; 
@(posedge clk) disable iff (!rst)
  $rose(state==A) ##1 C==16'H1FFF[->1] ##0 done |=> (state==B, $display(" A - B")) ;
endproperty : p_FSM_A_B_option1

property p_FSM_A_B_option2; 
@(posedge clk) disable iff (!rst)
  $rose(state==A) ##1 done[->1]   |=> (state==B, $display(" A - B")) ;
endproperty : p_FSM_A_B_option2

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
3

In reply to ben@SystemVerilog.us:

Thanks for your reply, I really appreciate this. Could you please explain what does the done[->1] do, specifically the →

Thanks

4

In reply to pagarwa5:
The [->1] is the goto operator.
goto repetition, Boolean ([->n], [|->n:m])
Rule: The goto repetition operator (Boolean[->n]) allows a Boolean expression (and not a sequence) to be repeated in either consecutive or non-consecutive cycles, but the Boolean expression must hold on the last cycle of the expression being repeated. The number of repetitions can be a fixed constant or a fixed range.
Note: b [->m] is equivalent to ( !b [*0:$] ##1 b)[*m]
thus,

b[->1] is equivalent to: !b[*0:$] ##1 b
b[->2] is equivalent to: !b[*0:$] ##1 b ##1 !b[*0:$] ##1 b
// You could have written the following 
$rose(state==A) ##1 done[->1]   |=> (state==B, $display(" A - B")) ;
// as
first_match($rose(state==A) ##[1:$] done[->1])   |=> (state==B, $display(" A - B")) ;

The first_match() is needed because SVA requires that each of the threads of a multithreaded antecedent be tested with its appropriate consequent.
With the goto, the cycle done==1’b1 guarantees that there could not be other threads with
!done ##1 done.

The general recommendation by experts in SVA is to avoid the first_match() if you can because it is more stylish and readable. I interpret a[->1} as the "first occurrence of “a”.

On a separate note, I strongly suggest that take a look at my package for dynamic delays and repeats. Even if you don’t use it right now, study the code, you’ll learn a few things.
https://verificationacademy.com/forums/systemverilog/sva-package-dynamic-and-range-delays-and-repeats

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy