> Offres de formation > Offres de thèses

Des preuves aux circuits - Conception d'architectures prédictibles RISC-V formellement vérifiées

Défi technologique : Cybersécurité : hardware et software (en savoir +)

Département : Département Systèmes et Circuits Intégrés Numériques (LIST)

Laboratoire : Laboratoire Environnement de Conception et Architecture

Date de début : 01-10-2023

Localisation : Saclay

Code CEA : SL-DRT-23-0474

Contact : Mihail.Asavoae@cea.fr

Les initiatives open-source pour la conception de matériel, comme RISC-V, font pression pour remplacer les méthodes traditionnelles de développement de matériel, car elles proposent des outils et des méthodologies pour accélérer ce processus de conception. Ce n'est pas seulement la productivité qui compte, c'est également important que les conceptions proposées répondent à des besoins spécifiques à un domaine. Par exemple, les domaines de l'automobile ou de l'avionique exigent que le comportement temporel soit fortement garanti, car c?est inacceptable que les délais soient dépassés. La présence d'un phénomène connu appelé anomalie temporelle (c'est-à-dire un comportement temporel indésirable) complique l'analyse du temps visant à garantir ces délais. Une façon d'aborder ce problème d'anomalies temporelles est de concevoir un matériel prédictible (c'est-à-dire sans anomalie), d'une manière systématique et fiable. Plus précisément, cette méthodologie est la suivante : utiliser un langage de description de matériel (HDL) spécialisé, intégré dans un cadre de vérification formelle afin de concevoir les caractéristiques de matériel RISC-V souhaité, puis énoncer et prouver les propriétés de matériel conçu, par exemple qu'il est exempt d'anomalies temporelles et enfin, générer un code matériel polyvalent (par exemple Verilog) pour FPGA ou silicium. Cette thèse vise à développer une telle méthodologie pour des c?urs RISC-V corrects par construction, facilement déployables dans les systèmes critiques. Deux contributions principales sont attendues : - explorer le compromis entre la prédictibilité du timing matériel et la performance matérielle observée avec d'exigences fortes comme l'absence d'anomalies temporelles. - explorer le compromis entre la prédictibilité du timing matériel et le support des chaînes d'outils logiciels (au niveau ISA) nécessqire lorsque certains mécanismes matériels axés sur la performance (et non prédictibles) sont autorisés lors de la conception. Ces contributions devraient être développées dans le système de preuve Coq en utilisant les cadres formels de matériel les plus avancés.

Voir toutes nos offres Télécharger l'offre (.zip)

Email Bookmark and Share