Can anyone check if assertion for 'ack goes high and stays high twice before the grant is issued. gnt must immediately follow ack.' correct or not? Or is there any easy approach?

SystemVerilog
1

ack_rose: assert property(@(posedge clk)
$rose(ack) |=> ack);

ack_gnt: assert property(@(posedge clk)
##2 ack |=> $rose(gnt));

EDA

2

The ack_rose assertions says that whenever ack rises, it must remain high for at least one clock cycle. Your description did not state that as a requirement. Should it be?

The ack_gnt assertion says starting after the second clock cycle, if ack is high, gnt must rise the next clock cycle. That only works when ack rises in the first clock cycle.

You probably want

 $rose(ack) ##0 ack[*2]|-> ##1 $rose(gnt))

or

 $rose(ack) |-> (ack&&!gnt)[*2] ##1 $rose(gnt))
3

Thanks dave_59,
I thought whenever ack goes high, it can remain high upto any clock cycles but whenever gnt goes high, before that ack stays high for 2 clock cycles.