Need help writing Systemverilog assertion (SVA) with req, busy, gnt

SystemVerilog
,
1

The DUT spec

A simple request/grant arbiter interface. All signals synchronous to clk, async active-low rst_n.

interface arb_if (input bit clk, input bit rst_n);
logic req; // requester asserts, holds until granted
logic gnt; // arbiter grants for exactly one cycle
logic [31:0] addr; // valid with req
logic busy; // arbiter cannot grant while high
logic err; // error pulse
logic [1:0] state; // 0=IDLE 1=ARB 2=GRANT 3=ERR
endinterface

I need to write an assertion that covers -
Req1 - Every req gets a gnt within 1 to 5 cycles.
Req2 -gnt must never assert while busy is high. Then: if busy is high when req arrives, the above shouldn’t apply until busy drops.

2

Please elaborate on "the above shouldn’t apply until busy drops"

For Req1 you could simply write

property req1;
 @(posedge clk) $rose(req) |-> ##[1:5] $rose(gnt);
endproperty

(1) It assumes that if gnt is asserted before req is asserted then the grant would be ignored.

(2) If gntif asserted on same clock as req and it’s de-asserted at next clock then the grant goes unnoticed