Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

Menhir: Generic High-Speed FPGA Model-Checker

Émilien Fournier 1 Ciprian Teodorov 1 Loïc Lagadec 1
1 Lab-STICC_ENSTAB_ CACS_MOCS
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance
Abstract : Among formal methods, model-checking offers a high-level of automation and can lower the cost of the verification process. Two preliminary studies on FPGA model-checking show a high-performance increase, thanks to the massive parallelism and precise memory control opportunities. However, these approaches rely on HDL-based ad-hoc model encoding, and miss the importance of decoupling the modeling language from the verification core, which greatly limits their usability. In this paper we propose Menhir, a new highly modular hardware model-checker, inspired by the architecture of software verification frameworks. Menhir is based on a generic language-verification interface which isolates the modeling-language semantics from the verification core, allowing their independent evolution. Menhir opens the architecture to the whole spectrum of modeling languages. Moreover, it proposes a polymorphic verification core, which offers a continuum between partial and exhaustive verification, with promising performances.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal-ensta-bretagne.archives-ouvertes.fr/hal-03028409
Contributeur : Marie Briec <>
Soumis le : vendredi 27 novembre 2020 - 15:38:38
Dernière modification le : mardi 8 décembre 2020 - 16:29:12

Identifiants

Citation

Émilien Fournier, Ciprian Teodorov, Loïc Lagadec. Menhir: Generic High-Speed FPGA Model-Checker. 2020 23rd Euromicro Conference on Digital System Design (DSD), Aug 2020, Kranj, Slovenia. pp.65-72, ⟨10.1109/DSD51259.2020.00022⟩. ⟨hal-03028409⟩

Partager

Métriques

Consultations de la notice

38