Verifying an Arbiter Circuit

Abstract--This paper presents the verification of an asynchronous arbiter modeled at the circuit level with non-linear ordinary differential equations. We use Brockett's annulus to represent the allowed families of continuous waveforms for input and output signals and show that the metastability filter of the arbiter can be understood as a "Brockett annulus transformer." Improvements to the Coho verification tool are described that reduce the over approximation errors when working with nonconvex reachable regions. The verification shows that the arbiter observes a four-phase handshake protocol with its clients and maintains mutual exclusion. We also show several liveness properties including bounded time response to uncontested requests and that grants are issued fairly.

• Type: Conference
• Year: 2008
• Where: FMCAD
• Authors: Chao Yan, Mark R. Greenstreet
• Keywords: Asynchronous Arbiter, Brockett Annulus Transformer, Brockett's Annulus, FMCAD 2008, Formal Methods