Ben Cohen of the SystemVerilog Assertions Handbook fame, posted a novel answer on how to check strict arbitration with SystemVerilog Assertions at Verification Academy. The core observation is that we can treat the request and grant bitvectors as an unsigned integers and compare then numerically when the highest priority is  the MSB.

Unfortunately, the solution uses a generate for loop which has a noticeable performance impact on my simulator, so I sat down to see if I could shoehorn in Ben’s solution into a single assertion. Ben’s assertion needs a temporary bitvector where the request[i] bit is placed at position i+1 with which he does the less than comparison. The alternative is to mask out the granted index from the request and do a less than comparison on that result. The less than operation must still succeed if the grant is correct. Thus the assertion can be written as:

a_arbiter_is_strict: assert property(@(posedge clk) req |-> (req & ~gnt) < gnt);

Naturally, strictness alone does not work correctly if the grant is not a one-hot vector, thus I always have the following assertions with any arbiter:

a_valid_signals: assert property(@(posedge clk) !$isunknown({req, gnt}));
a_valid_grant: assert property(@(posedge clk) (req != 0) == $onehot(gnt)); 
a_valid_no_grant: assert property(@(posedge clk) (req == 0) == (gnt == 0));
a_valid_grant_source: assert property(@(posedge clk) gnt |-> (gnt & req));

Note that the parenthesis are important. Instead of ==, I could also have used iff, but my EDA tools don’t support iff yet, so == it is.

Still, one question remains: What if the priority is from LSB to MSB? Here, the numerical idea no longer works, but we can still get by with a single assertion. The idea here is to use the power of two nature of the grant and mask out the higher order bits of the request with gnt-1.

a_arbiter_is_strict: assert property(@(posedge clk) req |-> (req & (gnt-1)) == 0);

And there you have it: Fast assertions for strict arbitration.