Verifying an Arbiter Circuit

13 years 6 months ago
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.
Chao Yan, Mark R. Greenstreet
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Authors Chao Yan, Mark R. Greenstreet
Comments (0)