Model-checking Synthesizable SystemVerilog Descriptions of Asynchronous Circuits
| Autor: | Aymane Bouzafour, Radu Mateescu, Hubert Garavel, Wendelin Serwe, Marc Renaudin |
|---|---|
| Přispěvatelé: | Tiempo SAS [Montbonnot Saint Martin], Construction of verified concurrent systems (CONVECS ), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), projet FUI SECURIOT2, European Project: 621221,EC:FP7:SP1-JTI,ENIAC-2013-2,THINGS2D0(2014) |
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
Model checking
[INFO.INFO-AR]Computer Science [cs]/Hardware Architecture [cs.AR] CADP Computer science Concurrency 02 engineering and technology LNT computer-aided design Asynchronous circuit asynchronous design Robustness (computer science) 0202 electrical engineering electronic engineering information engineering concurrency SystemVerilog formal verification Formal verification computer.programming_language [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] memory protection unit business.industry 020207 software engineering Deadlock model checking 020202 computer hardware & architecture asynchronous logic hardware design Asynchronous communication Embedded system [INFO.INFO-ES]Computer Science [cs]/Embedded Systems business computer |
| Zdroj: | ASYNC'18-24th IEEE International Symposium on Asynchronous Circuits and Systems ASYNC'18-24th IEEE International Symposium on Asynchronous Circuits and Systems, May 2018, Vienne, Austria ASYNC |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|