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 one single assertion that covers both requirements-
Req1 - Every req gets a gnt within 1 to 5 cycles.
Req2 -gnt must never assert while busy is high. So if busy is high when req arrives, gnt shouldnt be asserted 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

3

I modified the question!

4

I see three requirements, hence three assertions.

  1. req must hold until gnt
  2. gnt must never be asserted while busy is high
  3. gnt must be asserted for 1 cycle within 5 cycles of req and not busy
Req1: assert property (@(posedge clk)
  req |-> req until_with gnt
);
Req2: assert property (@(posedge clk)
  !(gnt && busy)
);
Req3: assert property (@(posedge clk iff !busy)
  $rose(req) |-> ##[1:5] (gnt ##1 !gnt)
);
5

Hi Dave,

Is this required ? It’s possible that req is asserted more than once ( 1st assertion → deasserted → 2nd assertion ) before the 1st gnt is asserted within 5 clocks of the 1st req

If the intention is to have a unique grant for each request, I believe Ben has a separate thread discussing this.

6

the requirement mentions that req should stay asserted until gnt

7

Thanks Dave! but is it possible to write this into a single assertion?

8

Oh I see that you have mentioned it as part of the comment

9

Keeping them as three separate assertions is usually easier to debug: each failure points to a specific requirement.

It’s easy to combine Req1 and Req2 into one assertion by and’ing the properties together. The third is a little harder because you’d have to create a local variable counter.

property Req1;
  req |-> req until_with gnt;
endproperty

property Req2;
  !(gnt && busy);
endproperty

property Req3;
  int n;
  ($rose(req) && !busy, n = 0) |=>
  ((busy || !gnt && n< 4), n = n + (!busy && !gnt))[*0:$]
  ##1 (gnt && !busy && n <= 4)  ##1 !gnt;
endproperty

assert property ( @(posedge clk)  Req1 and Req2 and Req3; );