Systemverilog Assertion scenario

SystemVerilog
1

Can anyone help to write assertion for the following scenario?
Whenever there is a ACK signal, GNT should be asserted.
property p;
@(posedge clk)
rose(ACK) |-->[1:] GNT
endproperty

But my doubt is that which if more than one time ACK got asserted, at that time how can I track which GNT corresponds to which ACK?
How to use a counter in this scenario?

2

As I can understand based on the question is following points :

  • Every ACK increases the counter.
  • Every GNT decreases the counter.
  • Ensures each ACK has a corresponding GNT.
module ack_gnt_assertion(output reg [7:0] ack_counter,input logic clk, reset, ACK, GNT);

  // Counter logic
  always @(posedge clk or posedge reset) begin
    if (reset) begin
      ack_counter = 0;
    end
    else begin
      if (ACK) begin 
        ack_counter = ack_counter + 1; // Increment on ACK assertion
      end
      if (GNT && ack_counter > 0) begin 
        ack_counter = ack_counter - 1; // Decrement on GNT assertion
      end
    end
  end

  // Assertion to check that GNT count should match ACK count
  property p_ack_gnt_match;
    @(posedge clk) disable iff (reset)
    (ACK |-> ##[0:$] GNT); // Ensure every ACK is eventually followed by a GNT
  endproperty

  a_ack_gnt_match: assert property (p_ack_gnt_match) else $error("ACK was asserted, but corresponding GNT did not appear!");

  // Assertion to ensure ACK count never exceeds GNT count
  property p_ack_gnt_balance;
    @(posedge clk) disable iff (reset)
    (ack_counter >= 0); // Counter should never be negative
  endproperty

  a_ack_gnt_balance: assert property (p_ack_gnt_balance) else $error("More GNTs detected than ACKs!");
    
endmodule