Hi,
I was playing around this piece of code with goto and non-consecutive. I noticed that this assertion never fails. I used strong and it failed when ack is 0. My question is lets say, if i want to check for each req, i need two ack's. In that case i am assuming i need to store the ack in a local variable and reset it whenever ack becomes 2? Is my understanding correct?
// req !ack !ack ack !ack !ack ack
property req_ack;
@(posedge clk) $rose(req) |=> (ack[->2]);
endproperty
or
// req !ack !ack ack !ack !ack ack !ack
property req_ack;
@(posedge clk) $rose(req) |=> (ack[=2]);
endproperty