Formal deadlock verification for click circuits

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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

4 Citaten (Scopus)

Samenvatting

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.
Originele taal-2Engels
Titel19th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2013, Santa Monica CA, USA, May 19-22, 2013)
UitgeverijIEEE Computer Society
Pagina's183-190
ISBN van geprinte versie978-1-4673-5956-6
DOI's
StatusGepubliceerd - 2013
Extern gepubliceerdJa

Vingerafdruk

Duik in de onderzoeksthema's van 'Formal deadlock verification for click circuits'. Samen vormen ze een unieke vingerafdruk.

Citeer dit