SV Assertions for Arbiter priority

SystemVerilog
, ,
7

In reply to Vignesh Raghavan:

Another solution, simpler, but without concurrent assertions.

module arbiter; 
//If I have to test a arbiter encoded arbiter with say, 4-inputs (request signals) and 4-outputs (grant signals), 
//What assertions are required for verifying this arbiter? 
   bit[15:0] req, grnt; 
   bit clk; 
    
 always @(posedge clk) begin 
    for (int i=15; i< 0; i--) begin 
       if (req[i]) 
          begin 
            assert(grnt[i]==1'b1 && $onehot(grnt)); // immediate assertion 
            break; 
          end 
    end 
  end 

  ap_zero_req: assert property(@(posedge clk) req==0 |-> grnt==0);