Using Assertions to test arbiter priority

Hi Gobuffs,

there are 2 excellent places to look at:

1) the IAL library (part of any IUS installation) contails a item called ial_arbiter. It is qualified for simulation.
2) in the IFV installation there are 4 vcomps, one of them is the vcomp_arbiter (IFV62-p001/doc/ifvref/example/meth/verif_docs/vcomp_arbiter.zip). It is qualified for formal verification.

Both of them can serve as starting point or template for your verification task.

Regards,
Joerg.

I can't find anything in ial_arbiter.vlib that answers my question.  Anyone else have any thoughts?

If your arbiter is a priority encoded arbiter. You should be able to create the following series of properties to ensure the priority encoding is working. These properties work on the premise that the currently granted channel has its req asserted and no other higher requests asserted. The goal of these properties is to give you a starting point to customize your own properties for your specific design.

Given:

4 input priority encoded arbiter with channels a, b, c, and d. Channel a has the highest priority and d the lowest.

// psl assert_A_should_be_granted: assert always {gnta} |-> {reqa};
// psl assert_B_should_be_granted: assert always {gntb} |-> {regb & !rega};
// psl assert_C_should_be_granted: assert always {gntc} |-> {reqc & !reqa & !reqb};
// psl assert_D_should_be_granted: assert always {gntd} |-> {reqd & !reqa & !reqb & !reqc};

You will probably have to fine tune these properties to handle other channels arbitrating for service while the current channel is granted but I hope you get the idea. In reality you may have to create aux signals that you can place into these properties to check for grants at the correct points in time in the arbitration.

In other words, the language behind assert_A_should_be_granted should read: IF channel a is granted I just have to make sure channel A requested service at the appropriate time.

For the property assert_D_should_be_granted it should read: If channel d is granted, I must have had no other higher priority channels requesting service.

Hope this helps.

JB