Seminar details

Abstract: Chip design is a highly complex task. It involves large teams of engineers with a wide range of skills. Their collective goal is to build chips that conform to their respective specifications, and that are bug-free. Despite the efforts made, it is not uncommon for manufactured chips to contain design errors that went unnoticed. Such scenario is a nightmare for semiconductor companies, for the cost of post-fabrication bug fixing is enormous. Companies hence tend to put even more resources toward test and verification than is spent on other design stages. One can clearly see the importance of early error detection in a circuit design project; the earlier an error is discovered, the less it would cost to fix it.
This thesis investigates the problem of error verification in integrated circuits. The design errors of interest are the so-called electrical errors, which are caused by violations of design rules specific to electrical properties. We study existing circuit verification techniques, to understand their limitations. We then introduce our own approaches and demonstrate their use to detect electrical properties violations in industrial circuits. This is achieved by first defining circuit semantics at transistor level, which can be dealt with as satisfiability modulo theories (SMT) problems. Properties (e.g., absence of an error) are then formalized and checked against the circuit formula using an SMT solver, namely Z3.
In addition to detecting electrical errors, we address the problem of the analysis of circuits reliability, and more specifically, that of finding the greatest lower bound for reliability of a circuit and the associated electrical state. In fact, the conditions in which a circuit is used determine its degradation rate. To each circuit state is associated a reliability as a function of age, for a given failure mechanism and related model parameters. Hence, finding the greatest lower bound for reliability boils down to identifying the least reliable circuit state at a given age. Such goal is reached by solving the corresponding optimization modulo theories (OMT) problem. The resulting information gives circuit designers solid guarantees on the lifetime of their circuits. These guarantees must be safe. Yet, the more realistic such information is, the better.
The approaches introduced in this work use circuit semantics that are derived from the actual circuit behavior. Different semantics, based on different levels of detail in modeling, are explored, implemented, validated against simulation (which is industry-standard in verifying the properties of interest), and compared with each other. The experimental evaluations conducted provide valuable insights on analysis precision-versus-performance tradeoffs.

Jury
- Emmanuelle Encrenaz, Professeure, Sorbonne Université, LIP6, Rapporteure
- Katell Morin-Allory, Professeure, Grenoble INP, TIMA, Rapporteure
- Arnaud Virazel, Professeur, Université de Montpellier, LIRMM, Examinateur
- Lars Hedrich, Professeur, Goethe-Universität, Institut für Informatik, Examinateur
- Xavier Urbain, Professeur, Université Claude Bernard Lyon 1, LIRIS, Examinateur
- Matthieu Moy, Maître de Conférences, Université Claude Bernard Lyon 1, LIP, Directeur de thèse
- Pascal Raymond, Chargé de Recherche, CNRS, Verimag, Co-encadrant de thèse
- Bruno Ferres, Maître de Conférences, Université Grenoble Alpes, Verimag, Co-encadrant de thèse
- Mehdi Khosravian, Ingénieur de Recherche, Aniah, Co-encadrant de thèse