// Accellera Copyright (c) 2006. All rights reserved.

//----------------------------------------------------------------------------
// CONTENTS (last updated: Mon Apr  7 11:59:55 BST 2008)
// ========
// 21.  About this file (SVA OVL assertions for arb1_* arbiter)
// 25.    - Standard defines
// 30. 
// 31.  Arbiter Assertions
// 35.    1) Never more than one grant
// 40.    2) No requests means no grants
// 46.    3) No unwanted grants
// 57.    4) Max bus usage
// 63.    5) Grant within N cycles
// 70.         a) 121 cycles (15x8 + 1)
// 81.         b) 136 cycles (15x9 + 1)
// 92.    6) No hogging the bus
//----------------------------------------------------------------------------


// INDEX: About this file (SVA OVL assertions for arb1_* arbiter)
// =====


// INDEX:   - Standard defines
// =====
`include "std_ovl_defines.h"


// INDEX:
// INDEX: Arbiter Assertions
// =====


// INDEX:   1) Never more than one grant
// =====
assert_zero_one_hot #(`OVL_ERROR,16,`OVL_ASSERT,"Never more than one grant") ovl_max_one_grant (clk, reset_n, grant);


// INDEX:   2) No requests means no grants
// =====
// This should also be covered by "No unwanted grants"
assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No requests means no grants") ovl_no_reqs_no_grants (clk, reset_n, ~|req, ~|grant);


// INDEX:   3) No unwanted grants
// =====
// Note: sva31a version uses generate to avoid verbose listing in vlog95
generate 
  genvar i;
  for (i=0; i<16; i++) begin: i_loop
     assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master") ovl_no_unwanted_grants (clk, reset_n, grant[i],  req[i]);
  end
endgenerate


// INDEX:   4) Max bus usage
// =====
// Simple round-robin schemes will fail this
assert_implication #(`OVL_ERROR,`OVL_ASSERT,"Max bus usage: one grant if any requests") ovl_max_usage (clk, reset_n, |req, |grant);


// INDEX:   5) Grant within N cycles
// =====
// Note: sva31a version uses generate to avoid verbose listing in vlog95
//
// Need the 136-cycle version as the 121-cycle version will fail in a simple round robin


// INDEX:        a) 121 cycles (15x8 + 1)
// =====
// Simple round-robin will fail this, due to servicing current master when bus quiet
generate
  genvar j;
  for (j=0; j<16; j++) begin: j_loop
     assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master within 121 cycles")  ovl_grant_within_121  (clk, reset_n, req[j],  ~req[j]  | grant[j]);
  end
endgenerate


// INDEX:        b) 136 cycles (15x9 + 1)
// =====
// Simple round-robin will pass this
generate
  genvar k;
  for (k=0; k<16; k++) begin: k_loop
     assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master within 136 cycles")  ovl_grant_within_136  (clk, reset_n, req[k],  ~req[k]  | grant[k]);
  end
endgenerate


// INDEX:   6) No hogging the bus
// =====
// If there are multiple requests, the master should not hog the bus
// and do a subsequent 8-cycle burst.
//
// This is different to the within-N proofs, as you might still hog the
// bus yet guarantee a response within N cycles (e.g. after two back-to-back
// bursts).
//
// Note: sva31a version uses $countones (vlog95 has a verbose expression)
wire aux_multiple_reqs = ($countones(req) > 1);
assert_change #(`OVL_ERROR,16,9,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Master cannot hog the bus if there are multiple requests") ovl_no_hogging
  (clk, reset_n, aux_multiple_reqs, ({16{~aux_multiple_reqs}} & grant));