Formal verification of arbiters using property strengthening and underapproximations

Arbiters are commonly used components in electronic systems to control access to shared resources. In this paper, we describe a novel method to check starvation in random priority-based arbiters. Typical implementations of random priority-based arbiters use pseudo-random number generators such as linear feedback shift registers (LFSRs) which makes them sequentially deep precluding a direct analysis of the design. The proposed technique checks a stronger bounded-starvation property; if the stronger property fails, we use the counterexample to construct an underapproximation abstraction. We next check the original property on the abstraction to check for its validity. We have found the approach to be a very effective bug hunting technique to reveal starvation issues in LFSR-based arbiters. We describe its successful application on formal verification of arbiters on a commercial processor design.