Suppose that I have a block whose input is a 8 bit wide request bus (called req_chnls) which carry requests from 8 sources. Also there is an internal signal called 'cursor' which can take any value from 0 to 7. Now lets assume that out of the 8 possible requests in the 'req_chnls' signal, requests 7,6,3,2,1 and 0 are asserted. The functionality of the block is that, out of the asserted (active) requests it will allow ONLY one of them to pass and the one that passes is the one closest and immediately above the cursor. For instance lets assume cursor is at 5 then out of the asserted requests (viz 7,6,3,2,1,0) the one that is closest and above (6 in this example) will be selected as the output.
How can verify this functionality solely using assertions. How will those properties look line?
