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.
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”.