Etudiant.es

Session 1 - Mercredi

Marco Rios, CH - EPFL

Titre : Le calcul en mémoire pour permettre l'intelligence artificielle en périphérie

L'analyse de données basée sur l'apprentissage machine nécessite de nouvelles architectures et des technologies révolutionnaires pour faire face à ses demandes écrasantes.

Considérant que la plupart des données nécessaires à la réalisation de tels algorithmes sont collectées en périphérie, l'informatique y est inévitablement poussée pour réduire la consommation d'énergie et la latence. De plus, le calcul en mémoire réoriente la structure de la mémoire pour permettre le calcul directement sur la hiérarchie de la mémoire, réduisant considérablement l'énergie dépensée pour les opérations de transfert de données. L'union de ces deux concepts permet le déploiement d'algorithmes très exigeants dans des puces à très faible consommation d'énergie et capacité de calcul.

Yifan Wang, FR - Université de Bordeaux

Titre : Caractérisation et modélisation de transistors à nanofils verticales de silicium sans jonction pour circuits logiques 3D

Dans ce résumé, nous avons étudié des transistors à nanofils verticales de silicium sans jonction (VNWFET) pour la conception de circuits logiques 3D. Suite à la validation du modèle compact développé pour les VNWFETs par les mesures réalisées sur plusieurs géométries, la scalabilité de différents paramètres physiques est analysée. Les effets thermiques et de piège du transistor sont ensuite explorés en analysant les résultats des mesures pulsés. 

Oussama Oulkaid, FR - Université Claude Bernard Lyon 1

Titre : Méthodes Formelles pour la Vérification Électrique de Circuits

Dans l’industrie des semi-conducteurs, les circuits intégrés sont fabriqués selon un long processus dont la vérification est essentielle. Il existe différents types de vérification de circuits: vérification fonctionnelle, propriétés temporelles, etc. Dans ma thèse, je m’intéresse à la vérification des règles de conception électrique. Ce type de vérification vise à détecter les erreurs électriques; par exemple, des court-circuits indésirables ou des nœuds à haute impédance. Une erreur électrique peut être exprimée par une configuration du circuit conduisant à un mauvais état. Le niveau d’abstraction qui permet de détecter ces erreurs est le niveau transistor. Les méthodes de vérification électrique dans l’état de l’art présentent certaines limites: à savoir traiter uniquement les circuits numériques pour en vérifier l’absence d’une erreur spécifique, ou l’exclusivité de l’analyse à un mode de fonctionnement spécifique du circuit.

L’objectif de ma thèse est l’application des méthodes de vérification formelle dans le contexte de la vérification électrique des circuits, tout en palliant les limites existantes. La méthode choisie consiste à coder les circuits en termes de formules logiques sur lesquelles il est possible de vérifier des propriétés électriques. Ainsi, vérifier l’absence d’une erreur E sur un circuit C revient à vérifier la satisfiabilité de la formule logique: C ∧(¬E). Dans un premier temps, nous proposons une sémantique de circuits permettant de traiter des circuits basés sur une topologie CMOS 1 . Enfin, le défi scientifique consiste à pousser les limites de l’analyse pour un passage à l’échelle, étant donné que le nombre de transistors dans une puce industrielle est au moins de l’ordre de milliards.

Clément Turck, FR - Université Paris Saclay

Titre : Conception de systèmes efficaces en énergie dédiés à l'inférence bayésienne exploitant des nouvelles technologies mémoires

L’objectif de la thèse est la conception et la fabrication de systèmes de circuits intégrés capables de réaliser des tâches d’intelligence artificielle en consommant très peu d’énergie. Nous utiliserons une nouvelle technologie du CEA LETI intégrant des mémoires émergentes à base de nano-composants, qui permet d’associer au plus près logique et mémoire non-volatile (memristors). Ces systèmes seront spécialisés pour le calcul d’inférence bayésienne dédié à des tâches de fusion de capteurs médicaux.

Flavio Ponzina, CH - EPFL

Titre : Convolutional neural networks ensembling for robust co-design methodologies in EdgeAI 

Embedded Ensembles of CNNs. My research thesis proposes E2CNN, an application-level methodology that transforms CNN models into ensemble-based equivalents, without incurring in memory and computing overheads. To achieve this goal, E2CNN uses pruning and replication: a single-instance model is first pruned to reduce complexity, and then, the obtained structure is replicated and trained to finally form the ensemble. At inference time, the individual output predictions are aggregated to produce the E2CNN output. When compared to single-instance models, E2CNN increases accuracy and robustness. In particular, I have investigated the resiliency of a proprietary industrial CNN where the use of sub-nominal memory voltage levels was introducing stuck-at faults in the memory cells. Results showed that accuracy degrades rapidly after a certain error density threshold. A more general analysis conducted on a larger pool of benchmarks revealed that a E2CNN can effectively tolerate higher error rates, thus supporting more aggressive voltage reductions. I evaluated E2CNN in more complex co-design solutions in the field of EdgeAI. 

Eduardo Tomasi Ribeiro, FR - CEA

Titre : Espace d’adressage unifié pour les calculateurs massivement parallèles à 128 bits

Le calcul haute performance (HPC) utilise des supercalculateurs composés de milliers de nœuds, chacun ayant des dizaines de processeurs organisés autour d’une mémoire partagée. Ces nœuds sont interconnectés par un réseau de communication à haut débit et faible latence. Leur infrastructure logicielle est composé d’un noyau Linux par nœud, et de middlewares spécialisés pour l’échange de données intra-nœuds. Les applications sont généralement décomposées en deux niveaux. Au niveau des nœuds, un processus est organisé en des multiples threads en mémoire partagée en utilisant, par exemple, OpenMP. Entre les nœuds, les processus d’une même application communiquent à travers le réseau de communication par des messages explicites grâce, par exemple, à MPI. D’autres modèles de programmation proposent de simplifier les applications HPC en offrant une vue unifiée de la mémoire virtuelle au niveau de la machine. Le modèle PGAS (Partitioned Global Address Space) offre un espace d’adressage à la fois partagé globalement par toute la machine, et partitionné de façon que chaque nœud soit responsable par une seule partie de cet espace. Par ailleurs, les applications HPC ont des besoins croissants en vitesse de calcul et en taille de données à traiter. L’augmentation de la taille des machines est telle que la mémoire globale au niveau de la machine risque de dépasser les 2⁶⁴ bytes de RAM dans la décennie à venir. La proposition d’une architecture à 128 bits par la communauté RISC-V permet de gérer de telles tailles de RAM et de repenser l’architecture logicielle de la machine . Notamment, elle nous permet d’envisager une virtualisation globale de la mémoire, qui serait commune entre tous les nœuds d’une même application.

Raphael Cardoso, FR - ECL

Titre : Photonic convolutional processor with phase-change materials

With powerful AI models reaching billions of parameters being processed by multiplications and accumulations (MACs), the demands for computing grow faster than electronic technologies can keep up. Thus, further improvements in computing require considerable paradigm shifts. In our work, we investigate an implementation of two paradigms: photonic computing and in-memory computing. We propose a new MAC cell for convolution in photonics with phase-change materials (PCMs), and compare it to the state-of-the art approach.

Session 2 - Jeudi

Rick Wertenbroek, CH - HEIG-VD

Titre : A reconfigurable Computational Storage Device for Green Big-Data

The last decade has seen an explosion in data generation, with fields such as astronomy, genomics, economics, or even online video hosting, each generating hundreds of petabytes of data each year. This new “Big-Data” era has allowed us to achieve incredible economic growth, make numerous scientific discoveries, and have infinite entertainment at our fingertips. However, handling these amounts of data requires high amounts of energy and it has been shown that data movement from storage to the processing unit can account for more than half of the energy spent. In face of the current energy situation, we introduce “Computational Storage” where we process the data directly in the storage medium with energy efficient solutions to allow for a greener compute solution.

Lamoussa Sanogo, FR - LAAS-CNRS

Titre : La reconfigurabilité et l'adaptabilité pour les objets communicants (IoT)

The number of connected devices in the context of the Internet of Things is growing up and has already reached several billion devices worldwide. However, the security of these devices remains a major concern. This paper address the possibility of finding a robust intrusion detection system for IoT devices independently of communication protocol used.

Léo De La Fuente, FR - Université de Grenoble

Titre : Optimisation de l’efficience énergétique du calcul proche mémoire pour la multiplication matricielle

Le calcul proche mémoire est un paradigme qui permet d’améliorer l’efficacité énergétique d’un système de traitement de données basé sur un processeur, grâce à la possibilité de réaliser des calculs « en place », réduisant ainsi la quantité de données qui transitent entre un processeur et une mémoire contenant des données à traiter. Les mises en œuvre ctuelles nécessitent toutefois d’avoir un trafic d’instructions parfois important entre processeur et mémoire. Mes travaux portent sur l’exécution de macro-opérations proche  mémoire, telles que la multiplication de matrices, afin d’optimiser leur bilan énergétique.

Pegdwende Romaric Nikiema, FR - Inria Rennes

Titre : Time-guaranteed and reliable execution for real-time multicore architectures

Les systèmes embarqués à forte contrainte de temps doivent garantir, outre l’exécution dans le temps im- parti, une exécution fiable. Les nouvelles architectures contribuent à l’augmentation de la complexité des processeurs multi-coeur qui rend difficile cette garantie temporelle. Par ailleurs, la forte diminution de la taille des transistors les rend très vulnérables aux fautes liées soit à l’environnement (rayonnement) soit à des attaques ciblées (EM). Le but de la thèse est d’apporter des moyens d’étude et d’estimation du WCET consciente des vulnérabilités de l’architecture et de concevoir des cores sous licence libre comme RISC-V, fiables pour des systèmes temps réel.

Simon Tollec, FR, Université Paris-Saclay

Titre : Exploration of Fault Effects on Formal RISC-V Microarchitecture Models

For more than ten years, a lot of work has been addressing the characterization of fault effects given specific equipment and a given target processor [2]–[5]. Such characterization is conducted following a black-box or grey-box approach as proper documentation is not publicly available. Moreover, only limited information can be retrieved after a fault injection, typically the content of the general purpose registers and memory. Fault effects are eventually expressed at the Instruction Set Architecture (ISA) level and thus known as ISA-level fault models. These comprise instruction or operand corruption [2], [4], instruction skip [2], [3], [5], test inversion, instruction replay [3], [6], etc. The ISA-level fault model is convenient for designing software protections or performing vulnerability analyses because it effectively abstracts the target hardware and still encompasses a broad set of faulty behaviors. However, some other effects escape this ISA-level modeling and thus remain unexplained. As an example, Proy et al. [7] classified as magic edges some effects observed on a real use case but undetected in their fault characterization based on specific test codes. Some faults inside the microarchitecture can not be explained at the ISA level, as shown by Laurent et al. [8]. For security evaluation purposes, there is thus a need for vulnerability analyses to consider both software and hardware (i.e., microarchitecture) in order to analyze the fault effects. Processor source code is now available through open hardware initiatives making such white-box vulnerability analyses possible. Vulnerability analyses can be performed using simulation tools. Nevertheless, due to the extensive domain of the data input and possible faults, simulation requires techniques for pruning the search space to eventually find a vulnerability. Formal verification (e.g., model checking) is advantageous because it allows abstracting the input data or the fault value by using symbolic evaluation to cover a wider range of analyses. Besides, the verification process is guided towards identifying counterexamples (i.e., vulnerabilities), whereas simulation requires an exhaustive search through all possibilities. Thus, we argue that formal verification provides a strong foundation to systematically explore hardware/software systems in order to comprehensively characterize faults. While some formal approaches at binary code or ISA level have been proposed [9]–[11], to the best of our knowledge, there exists no formal approach for studying the fault injection effects considering both software and hardware.

The presentation (based on the accepted paper to FDTC 2022 [1]) introduces a formal verification-based workflow for modeling software/hardware systems in order to explore the effects of fault injections and evaluate the system’s robustness to fault injections. Our workflow starts from a binary program (an .ELF file), a Register Transfer Level (RTL) implementation of a processor core and memory, and configuration files to specify the fault injection settings and the security property of interest. Whenever a fault vulnerability is identified, the workflow generates a counterexample as a Value Change Dump (VCD) file, presenting the processor signals and the corresponding hardware-level trace. We illustrate this workflow (Figure 1) on four versions of a PIN authentication code [12], embedding different software countermeasures. The code is symbolically evaluated on two implementations of the RISC-V CV32E40P core: the original implementation from the OpenHW group [13] and an implementation that integrates protection of the pipeline control signals [14]. On the original, unprotected core, our formal workflow exposes various vulnerabilities, including previously unknown ones. E.g., a single fault injection in the PFB can lead to various effects with immediate and potentially longer-term consequences as the microarchitectural state is altered. On the other hand, on the protected core, the formal verification confirms the effectiveness of the proposed countermeasures.

Joachim Tapparel, CH - EPFL

Titre : Étude de Transcepteur Avancé et Prototypage pour Réseaux Étendu à Basse Consommation

Que ce soit dans la manufacture, l’agriculture ou la surveillance environnementale, un nouveau type de réseau sans fil a récemment connu une croissance importante : les réseaux étendus à basse consommation (LPWAN). Ces réseaux sont destinés principalement à la communication entre capteurs et actionneurs, privilégiant une faible consommation énergétique et une grande distance de communication au détriment du débit. Afin d’être utile à long terme, cette technologie doit supporter une densification importante ainsi que proposer de nouvelles fonctionnalités telles que la localisation. Nous présentons ici les aspects étudiés pour pallier aux nombres croissants de collisions et pour réduire la consommation énergétique.

Informations utiles

Les étudiants aux cycles supérieures sont invités à envoyer un résumé de leurs travaux de thèse (1 page). Les candidatures sont à envoyer directement à :

Les étudiants sélectionnés pourront présenter leurs travaux en session plénière (180 secondes par présentation) et lors d'une session poster. Un prix symbolique sera remis à l'auteur-e de la meilleure présentation.

Les soumissions arrivées avant le 5 décembre au soir recevront un soutien financier qui sera défini en fonction du nombre de candidatures retenues.

Modèle Word pour le résumé : Télécharger le fichier