Formal verification of correctness and performance of random priority-based arbiters