// Accellera Copyright (c) 2006. All rights reserved. //---------------------------------------------------------------------------- // CONTENTS // ======== // 22. About this file (Verilog OVL assertions for arb1_* arbiter) // 26. - Standard defines // 31. // 32. Arbiter Assertions // 36. 1) Never more than one grant // 41. 2) No requests means no grants // 47. 3) No unwanted grants // 69. 4) Max bus usage // 75. 5) Grant within N cycles // 83. a) 121 cycles (15x8 + 1) // 104. b) 136 cycles (15x9 + 1) // 125. 6) No hogging the bus // 141. - aux_multiple_reqs (avoids 16 OVL instances) //---------------------------------------------------------------------------- // INDEX: About this file (Verilog 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 // Could also use array-of-instances in vlog95 (see LRM section 12.1.2) but not all tools support this assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 0") ovl_no_unwanted_grants_m0 (clk, reset_n, grant[0], req[0]); assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 1") ovl_no_unwanted_grants_m1 (clk, reset_n, grant[1], req[1]); assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 2") ovl_no_unwanted_grants_m2 (clk, reset_n, grant[2], req[2]); assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 3") ovl_no_unwanted_grants_m3 (clk, reset_n, grant[3], req[3]); assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 4") ovl_no_unwanted_grants_m4 (clk, reset_n, grant[4], req[4]); assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 5") ovl_no_unwanted_grants_m5 (clk, reset_n, grant[5], req[5]); assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 6") ovl_no_unwanted_grants_m6 (clk, reset_n, grant[6], req[6]); assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 7") ovl_no_unwanted_grants_m7 (clk, reset_n, grant[7], req[7]); assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 8") ovl_no_unwanted_grants_m8 (clk, reset_n, grant[8], req[8]); assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 9") ovl_no_unwanted_grants_m9 (clk, reset_n, grant[9], req[9]); assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 10") ovl_no_unwanted_grants_m10 (clk, reset_n, grant[10], req[10]); assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 11") ovl_no_unwanted_grants_m11 (clk, reset_n, grant[11], req[11]); assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 12") ovl_no_unwanted_grants_m12 (clk, reset_n, grant[12], req[12]); assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 13") ovl_no_unwanted_grants_m13 (clk, reset_n, grant[13], req[13]); assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 14") ovl_no_unwanted_grants_m14 (clk, reset_n, grant[14], req[14]); assert_implication #(`OVL_ERROR,`OVL_ASSERT,"No unwanted grants for master 15") ovl_no_unwanted_grants_m15 (clk, reset_n, grant[15], req[15]); // 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 // Could also use array-of-instances in vlog95 (see LRM section 12.1.2) but not all tools support this // // 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 assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 0 within 121 cycles") ovl_grant_within_121_m0 (clk, reset_n, req[0], ~req[0] | grant[0]); assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 1 within 121 cycles") ovl_grant_within_121_m1 (clk, reset_n, req[1], ~req[1] | grant[1]); assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 2 within 121 cycles") ovl_grant_within_121_m2 (clk, reset_n, req[2], ~req[2] | grant[2]); assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 3 within 121 cycles") ovl_grant_within_121_m3 (clk, reset_n, req[3], ~req[3] | grant[3]); assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 4 within 121 cycles") ovl_grant_within_121_m4 (clk, reset_n, req[4], ~req[4] | grant[4]); assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 5 within 121 cycles") ovl_grant_within_121_m5 (clk, reset_n, req[5], ~req[5] | grant[5]); assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 6 within 121 cycles") ovl_grant_within_121_m6 (clk, reset_n, req[6], ~req[6] | grant[6]); assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 7 within 121 cycles") ovl_grant_within_121_m7 (clk, reset_n, req[7], ~req[7] | grant[7]); assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 8 within 121 cycles") ovl_grant_within_121_m8 (clk, reset_n, req[8], ~req[8] | grant[8]); assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 9 within 121 cycles") ovl_grant_within_121_m9 (clk, reset_n, req[9], ~req[9] | grant[9]); assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 10 within 121 cycles") ovl_grant_within_121_m10 (clk, reset_n, req[10], ~req[10] | grant[10]); assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 11 within 121 cycles") ovl_grant_within_121_m11 (clk, reset_n, req[11], ~req[11] | grant[11]); assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 12 within 121 cycles") ovl_grant_within_121_m12 (clk, reset_n, req[12], ~req[12] | grant[12]); assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 13 within 121 cycles") ovl_grant_within_121_m13 (clk, reset_n, req[13], ~req[13] | grant[13]); assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 14 within 121 cycles") ovl_grant_within_121_m14 (clk, reset_n, req[14], ~req[14] | grant[14]); assert_frame #(`OVL_ERROR,0,121,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 15 within 121 cycles") ovl_grant_within_121_m15 (clk, reset_n, req[15], ~req[15] | grant[15]); // INDEX: b) 136 cycles (15x9 + 1) // ===== // Simple round-robin will pass this assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 0 within 136 cycles") ovl_grant_within_136_m0 (clk, reset_n, req[0], ~req[0] | grant[0]); assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 1 within 136 cycles") ovl_grant_within_136_m1 (clk, reset_n, req[1], ~req[1] | grant[1]); assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 2 within 136 cycles") ovl_grant_within_136_m2 (clk, reset_n, req[2], ~req[2] | grant[2]); assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 3 within 136 cycles") ovl_grant_within_136_m3 (clk, reset_n, req[3], ~req[3] | grant[3]); assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 4 within 136 cycles") ovl_grant_within_136_m4 (clk, reset_n, req[4], ~req[4] | grant[4]); assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 5 within 136 cycles") ovl_grant_within_136_m5 (clk, reset_n, req[5], ~req[5] | grant[5]); assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 6 within 136 cycles") ovl_grant_within_136_m6 (clk, reset_n, req[6], ~req[6] | grant[6]); assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 7 within 136 cycles") ovl_grant_within_136_m7 (clk, reset_n, req[7], ~req[7] | grant[7]); assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 8 within 136 cycles") ovl_grant_within_136_m8 (clk, reset_n, req[8], ~req[8] | grant[8]); assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 9 within 136 cycles") ovl_grant_within_136_m9 (clk, reset_n, req[9], ~req[9] | grant[9]); assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 10 within 136 cycles") ovl_grant_within_136_m10 (clk, reset_n, req[10], ~req[10] | grant[10]); assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 11 within 136 cycles") ovl_grant_within_136_m11 (clk, reset_n, req[11], ~req[11] | grant[11]); assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 12 within 136 cycles") ovl_grant_within_136_m12 (clk, reset_n, req[12], ~req[12] | grant[12]); assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 13 within 136 cycles") ovl_grant_within_136_m13 (clk, reset_n, req[13], ~req[13] | grant[13]); assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 14 within 136 cycles") ovl_grant_within_136_m14 (clk, reset_n, req[14], ~req[14] | grant[14]); assert_frame #(`OVL_ERROR,0,136,`OVL_IGNORE_NEW_START,`OVL_ASSERT,"Grant master 15 within 136 cycles") ovl_grant_within_136_m15 (clk, reset_n, req[15], ~req[15] | grant[15]); // 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: vlog95 uses auxiliary logic to avoid multiple instances, but sva31a // can simplify this with $countones. // 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)); // INDEX: - aux_multiple_reqs (avoids 16 OVL instances) // ===== // Auxiliary logic: more than one request asserted wire aux_multiple_reqs; assign aux_multiple_reqs = ~( (req == 16'b1000000000000000) | (req == 16'b0100000000000000) | (req == 16'b0010000000000000) | (req == 16'b0001000000000000) | (req == 16'b0000100000000000) | (req == 16'b0000010000000000) | (req == 16'b0000001000000000) | (req == 16'b0000000100000000) | (req == 16'b0000000010000000) | (req == 16'b0000000001000000) | (req == 16'b0000000000100000) | (req == 16'b0000000000010000) | (req == 16'b0000000000001000) | (req == 16'b0000000000000100) | (req == 16'b0000000000000010) | (req == 16'b0000000000000001) | (req == 16'b0000000000000000) );