Proving Newtonian Arbiters Correct, almost surely

This paper presents the verification of safety and liveness for two arbiters modeled with differential equations. The first is a “toy” arbiter, whose model was chosen for its tractability; the second is Seitz’s nMOS arbiter, chosen as an example of a widely used and studied design. Because an arbiter cannot be guaranteed to respond correctly in any boundedamount of time, we verify liveness in an almost surely sense—with probability 1, the arbiter eventually grants some pending request. Our analysis is more general than previously published results in that we allow the inputs of the arbiter to vary while the arbiter is in the metastable region, and we give conditions that ensure liveness even in the presence of such variations.