In reply to Timus:
In reply to ben@SystemVerilog.us:
Yes you got the requirments correct.just one addition ACK should come before timeout or even present before the state ABS
But I wanted two write 2 assertions.
1.FSM is stays in the same state if ACK is not there before timeout.
// This does cover "the same state if ACK is not there before timeout"
// Conditions for state to go into BBS without the ack
ap_ABS_till_BBS: assert property(@ (posedge clk)
$rose(state==ABS) |-> ##1 state==ABS[*1:99] ##0 state==BBS);
2.FSM moves to next state onc_e either ACK is present or if ACK is not present, it should move to next state after timeout.(is it possible to write in same assertion)
// Previous assertion addresses "FSM moves to next state onc_e either ACK is present"
// Conditions for state to go into BBS with the ack
ap_ABS2BBS: assert property(@ (posedge clk)
first_match($rose(state==ABS) ##1 state==ABS[*1:99] ##0 ack) |-> state==BBS);
It is best to write multiple small assertions rather than one big one. If you insist on one big one, then convert the above two assertions into two separate properties (e.g., P1, P2) then write an assertion with (P1 or P2). There, you got one assertion with 2 ORed properties.
Harder to debug though!
:)