Formal deadlock verification for click circuits

F. Verbeek; S.J.C. Joosten; J. Schmaltz

doi:10.1109/ASYNC.2013.21

Formal deadlock verification for click circuits

F. Verbeek, S.J.C. Joosten, J. Schmaltz

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

4 Citations (Scopus)

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.

Original language	English
Title of host publication	19th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2013, Santa Monica CA, USA, May 19-22, 2013)
Publisher	IEEE Computer Society
Pages	183-190
ISBN (Print)	978-1-4673-5956-6
DOIs	https://doi.org/10.1109/ASYNC.2013.21
Publication status	Published - 2013
Externally published	Yes

Access to Document

10.1109/ASYNC.2013.21

Cite this

@inproceedings{f5f7d640601f4d90afe527f669a4be9b,

title = "Formal deadlock verification for click circuits",

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 = "F. Verbeek and S.J.C. Joosten and J. Schmaltz",

year = "2013",

doi = "10.1109/ASYNC.2013.21",

language = "English",

isbn = "978-1-4673-5956-6",

pages = "183--190",

booktitle = "19th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2013, Santa Monica CA, USA, May 19-22, 2013)",

publisher = "IEEE Computer Society",

address = "United States",

}

Formal deadlock verification for click circuits. / Verbeek, F.; Joosten, S.J.C.; Schmaltz, J.
19th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2013, Santa Monica CA, USA, May 19-22, 2013). IEEE Computer Society, 2013. p. 183-190.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Formal deadlock verification for click circuits

AU - Verbeek, F.

AU - Joosten, S.J.C.

AU - Schmaltz, J.

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

U2 - 10.1109/ASYNC.2013.21

DO - 10.1109/ASYNC.2013.21

M3 - Conference contribution

SN - 978-1-4673-5956-6

SP - 183

EP - 190

BT - 19th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2013, Santa Monica CA, USA, May 19-22, 2013)

PB - IEEE Computer Society

ER -

Formal deadlock verification for click circuits

Abstract

Access to Document

Fingerprint

Cite this