In reply to ben@SystemVerilog.us:
Hi Ben,
The above logic seems ok to verify a priority-encoded arbiter.
- Only 1 grant is active in a clock cycle.
- The active grant corresponds to the (higher numbered bit in) active request.
- No grant is issued if no request is active.
Here, a particular active request will remain active until it sees a corresponding active grant in the sampling clock edge.
As I understand, Since at every sampling clock, the local variable v to the property is created newly and used for asserting if the property holds, hence, v will be initialised to 0 when bit[16:0] v; statement is executed. By default, SV assigns ‘0’ to 2-state variables (here, bit[16:0] v).
Is that the reason behind why we can ignore v=0 in the property expression?