In reply to Timus:
Errata : should be two separate properties (e.g., P1, P2) then write an assertion with (P1 and P2). There, you got one assertion with 2 ANDed properties.
$rose(state==ABS) |->
##1 state==ABS[*1:99] ##0 state==BBS);
// says if New ABS then starting from the next clock
// state==ABS is repeat 1 up to 99 more cycles
// until state==BBS
// a[*1:2] ##0 b is same as
// (a ##0 b) or (a ##1 a ##0 b)
// No, it does not fails if ack is present .
// ack is not even in this assertion.
// FSM should move to next state if ACK is not present in this case ,
// It does.
// NO on "But only after 100 clk cycles."
// This assertion allows it to check before timeout
// you need to understand the meaning of
// a[*1:2] ##0 b, see above; there is an "or"