//----------------------------------------------------------------------------
// CONTENTS
// ========
// 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
//
// This version demonstrates the improved readability/usability from
// the proposed SV extensions:
// - Checkers: ugly separation between # parameters and ports is removed,
//   and only non-default values need to be specified
// - Global default clock and reset:  these don't need to be in each assert
// - Variable typing: eliminates need for redundantly specifying widths 
// - This also allows single-bit asserts to operate on full vectors,
//   instead of having  to 'generate' an array of assertions.  The
//   reduced # of insts will probably give simulation performance
//   benefits as well.	
//
// Even though only a small subset of the extensions are applied in this
// example, I think the benefits at the user level are very clear.
//----------------------------------------------------------------------------


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


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

// Global clock and reset should be defined in calling RTL

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


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

ovl_max_one_grant:  assert_zero_one_hot(
		.msg("Never more than one grant"),.vec(grant));


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

ovl_no_reqs_no_grants:  assert_implication(
		.msg("No requests means no grants"), .ant(~|req),
	        .cons(~|grant));


// INDEX:   3) No unwanted grants
// =====
// WAS
// generate 
//  genvar i;
//  for (i=0; i<16; i++) begin: i
//     assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master") ovl_no_unwanted_grants (clk, reset_n, grant[i],  req[i]);
//  end
//endgenerate

ovl_no_unwanted_grants:  assert_implication(
		.msg("No unwanted grants for master"),
		.ant(grant), .cons(req)); 


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

ovl_max_usage:  assert_implication( 
		.msg("Max bus usage: one grant if any requests"),
		.ant(|req), .cons(|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
// WAS:
//generate
//  genvar j;
//  for (j=0; j<16; j++) begin: j
//     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

ovl_grant_within_121:  assert_frame(
		.msg("Grant master within 121 cycles"), .maxtime(121), 
	        .start_event(req), .test_expr(~req | grant));



// INDEX:        b) 136 cycles (15x9 + 1)
// =====
// Simple round-robin will pass this
// WAS: generate
//  genvar k;
//  for (k=0; k<16; k++) begin: k
//     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

ovl_grant_within_136:  assert_frame (
	      .msg("Grant master within 136 cycles"), .maxtime(136), 
	      .start_event(req), .test_expr(~req | grant));


// 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);

// WAS: 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));

ovl_no_hogging:  assert_change( 
	.msg("Master cannot hog the bus if there are multiple requests"),
	.maxtime(9), .start_event(aux_multiple_reqs),
	.vec((16{~aux_multiple_reqs}) & grant));