Formal Verification of an Arbiter Circuit
The work
| Authors | Chao Yan; Mark Greenstreet; Jochen Eisinger |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2010 |
| Citekey | yan2010formal |
Where it appeared
| Published in | 2010 IEEE Symposium on Asynchronous Circuits and Systems |
|---|---|
| Publisher | IEEE |
| Pages | 165--175 |
Identifiers
| DOI | 10.1109/async.2010.25 |
|---|
Access
| Landing page | https://doi.org/10.1109/async.2010.25 |
|---|
Abstract
We present the circuit-level verification of a common arbiter circuit. To perform this verification, we address three issues. First, we present a specification for the arbiter and show how this specification amounts to a set of topological constraints on trajectories of the continuous model. Second, we show that computing bounding sets for these trajectories is complicated by stiffness of the differential equation model and present novel techniques for handling stiff equations in a formal verification context. Finally, we note that while no arbiter can be guaranteed to always grant a pending request, we can show liveness in the presence of concurrent requests in an "almost surely" sense.
A copy is held
pdf, 1.7 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-09-15 20:54 UTC |
| Approved by | a person 2026-09-15 20:56 UTC |
Filed under
Cite it as
@inproceedings{yan2010formal,
title = {Formal Verification of an Arbiter Circuit},
author = {Chao Yan and Mark Greenstreet and Jochen Eisinger},
year = {2010},
booktitle = {2010 IEEE Symposium on Asynchronous Circuits and Systems},
publisher = {IEEE},
pages = {165--175},
doi = {10.1109/async.2010.25},
}
This record lives at https://refs.drheap.org/yan2010formal/ and will keep doing so.