Formal verification of arbiters using property strengthening and underapproximations
Gadiel Auerbach, Fady Copty, Viresh Paruthi · 2010
Abstract—Arbiters are commonly used components in elec-tronic systems to control access to shared resources. In this paper, we describe a novel method to check starvation in ran-dom 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 counter-example 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. I.