Patent ID: 8370553

Claim:
A method, in a data processing system, for formally verifying random priority-based arbiters, the method comprising: monitoring, by a processor, a set of input ports and a set of output ports to and from a random priority-based arbiter operating under a predefined property for a first predetermined time period; determining, by the processor, whether the random priority-based arbiter is blocking one of the set of output ports or the set of input ports from either sending or receiving data for the first predetermined time period using a random seed; responsive to the first predetermined time period expiring before the processor determines whether the random priority-based arbiter is blocking one of the set of output ports or the set of input ports using the random seed, determining, by the processor, whether the random priority-based arbiter is blocking one of the set of output ports or the set of input ports within a second predetermined time period using the random seed and at least one of property strengthening or underapproximation; and responsive to the processor determining that the random priority-based arbiter satisfies a non-blocking specification such that not one of the set of output ports or the set of input ports is blocked within the second predetermined time period using the random seed and either property strengthening or underapproximation, validating, by the processor, that the random priority-based arbiter satisfies the non-blocking specification.