Skip to Content

Formal deadlock verification for click circuits

Posted on

Authors:

  • Verbeek, Freek
  • Joosten, Sebastiaan J. C.
  • Schmaltz, Julien

Published in: Asynchronous Circuits and Systems (ASYNC), 2013 IEEE 19th International Symposium on pp 183–190

DOI: 10.1109/ASYNC.2013.21

Paper

Abstract:

Scalable formal verification constitutes an important challenge for the design of complicated asynchronous circuits. Deadlock freedom is a property that is desired but hard to verify. It is an emergent property that has to be verified monolithically. We propose to use Click, an existing library of asynchronous primitives, for verification. We present the automatic extraction of abstract SAT/SMT instances from circuits consisting of Click primitives. A theory is proven that opens the possibility of applying existing deadlock verification techniques for synchronous communication fabrics to asynchronous circuits.

BibTeX entry:

@inproceedings{Verbeek13,
 abstract = {Scalable formal verification constitutes an important challenge for the design of complicated asynchronous circuits. Deadlock freedom is a property that is desired but hard to verify. It is an emergent property that has to be verified monolithically. We propose to use Click, an existing library of asynchronous primitives, for verification. We present the automatic extraction of abstract SAT/SMT instances from circuits consisting of Click primitives. A theory is proven that opens the possibility of applying existing deadlock verification techniques for synchronous communication fabrics to asynchronous circuits.},
 author = {Verbeek, Freek and Joosten, Sebastiaan Jozef Christiaan and Schmaltz, Julien},
 bdsk-url-1 = {https://doi.org/10.1109/ASYNC.2013.21},
 booktitle = {Asynchronous Circuits and Systems (ASYNC), 2013 IEEE 19th International Symposium on},
 doi = {10.1109/ASYNC.2013.21},
 month = {May},
 organization = {IEEE},
 pages = {183--190},
 title = {Formal deadlock verification for click circuits},
 year = {2013}
}