Advisors : Pascal Raymond and Bruno Ferres
External advisor : Matthieu Moy (LIP, Lyon)
Context
Aniah is a start-up that offers tools for analyzing integrated circuits at an industrial scale. Aniah has introduced algorithms that significantly push the boundaries of the size of analyz able circuits, from a few hundred thousand elements to several trillion.
Aniah is working in collaboration with the Laboratoire de l’Informatique du Parallélisme (LIP) and the Verimag laboratory to consolidate and generalize its approach by supplementing its practical results with a theoretical backbone.
We already carried-out one post-doc and started one Ph.D on the topic. One of the objectives of this study is to explore the applicability of state-of-the-art model-checking techniques to the problem of circuit electric verification. In particular, we are now interested in improving our current approach to make it possible to handle efficiently hierarchical circuits.
Objectives of the internship
The objective of the internship is to implement several heuristics that can be used for modular analysis of circuits — i.e. abstracting analysis results on sub-circuits to reason about the whole hierarchy. It is then expected that the candidate will :
- develop a theoretical basis to reason about sub-circuit in the existing SMT-based semantics
- implement the derived abstraction of sub-circuit in the OCaml prototype of the project, to enable modular analysis
- benchmark the performances of the approach
- propose various optimization to improve the abstraction
Contact
For more information, please see the proposal attached. If you are interested in this internship, do not hesitate to contact the advisors.
