Formal Verification of Correctness and Performance of Random Priority-based Arbiters

Arbiters are one of the building blocks of electronic systems, and play an important role in their performance. We describe a novel method to formally verify correctness and performance of random priority-based arbiters. We define a property of random number sequences, called Complete Random Sequence (CRS), to characterize bounded fairness properties of random number generators and random priority-based arbiters. We utilize the notion of CRS to outline a three step verification method to establish deadlock-free operation of the arbiters, and to accurately quantify the request-to-grant delays to verify conformance to the design specifications. The proposed verification method may additionally be leveraged for tuning of systems using random priority-based arbiters and pseudo-random number generators such as linear feedback shift registers (LFSRs). We have successfully applied the proposed methodology to verify a host of cache arbiters and interconnection network controllers.

By: Krishnan Kailas; Viresh Paruthi; Brian Monwai

Published in: Proceedings of 2009 International Conference on Formal Methods in Computer-Aided Design (FMCAD 2009)Piscataway, NJ, IEEE,, p.101-7 in 2009

Please obtain a copy of this paper from your local library. IBM cannot distribute this paper externally.

Questions about this service can be mailed to reports@us.ibm.com .