Model-checking Synthesizable SystemVerilog Descriptions of Asynchronous Circuits

Abstract : Asynchronous circuits have key advantages in terms of low energy consumption, robustness, and security. However , the absence of a global clock makes the design prone to deadlock, livelock, synchronization, and resource-sharing errors. Formal verification is thus essential for designing such circuits, but it is not widespread enough, as many hardware designers are not familiar with it and few verification tools can cope with asyn-chrony on complex designs. This paper suggests how an industrial design flow for asynchronous circuits, based upon the standard HDL SystemVerilog, can be supplemented with formal verification capabilities rooted in concurrency theory and model-checking technology. We demonstrate the practicality of our approach on an industrial asynchronous circuit (4000 lines of SystemVerilog) implementing a memory protection unit.
Document type :
Conference papers
ASYNC'18 - 24th IEEE International Symposium on Asynchronous Circuits and Systems , May 2018, Vienne, Austria
Liste complète des métadonnées

Cited literature [54 references]  Display  Hide  Download

https://hal.inria.fr/hal-01777093
Contributor : Hubert Garavel <>
Submitted on : Tuesday, April 24, 2018 - 4:24:32 PM
Last modification on : Wednesday, April 25, 2018 - 9:14:01 AM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2018-10-24

Please log in to resquest access to the document

Identifiers

  • HAL Id : hal-01777093, version 1

Collections

Citation

Aymane Bouzafour, Marc Renaudin, Hubert Garavel, Radu Mateescu, Wendelin Serwe. Model-checking Synthesizable SystemVerilog Descriptions of Asynchronous Circuits. ASYNC'18 - 24th IEEE International Symposium on Asynchronous Circuits and Systems , May 2018, Vienne, Austria. 〈hal-01777093〉

Share

Metrics

Record views

197