SV Assertions for Arbiter priority

SystemVerilog
, ,
11

Another Solution from SVA cookbook videos. Adding so that it is indexed.
SVA Cookbook Link
Assumes the fixed priority 0 > 1 > 2 > 3 > 4 > 5

If a high priority req[i] is asserted then gnt[i] is not seen before the low priority gnt[j], such a sequence should not be seen.


property priority_arb(i,j);
   @(posedge clk) disable iff(rst)
      not( ((j>i) && req[i]) ##1 ( !gnt[i] throughout (gnt[j][->1]) ) );
endproperty

generate
genvar i,j;
   for(i=0; i<6; i++)
      for(j=0; j<6; j++)
          assert property(priority_arb(i,j));
      end
    end
endgenerate

Have not tested it though!!!