Travailler à TIMA
Propositions de stages
Intégration d’un composant mémoire multi-ports dans un outil de synthèse d’architecture
Equipe : SLS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Date de début : printemps 2012
Durée : 5 à 6 mois
Profil : Consulter la fiche.
Personne à contacter : Olivier Muller, Adrien Prost-Boucle et Frédéric Rousseau
Modélisation haut niveau d’un capteur de vision CMOS sur SystemC-AMS
Equipe : CIS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Date de début : 2012
Profil : Consulter la fiche.
Personne à contacter : Gilles SICARD et Hawraa AMHAZ Tél : 04-76-57-46-42 fax : 04-76-57-49-81
Modélisation en VHDL-AMS de plusieurs architectures de pixel CMOS
Equipe : CIS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Date de début : 2012
Profil : Consulter la fiche.
Personne à contacter : Gilles SICARD et Hawraa AMHAZ Tél : 04-76-57-46-42 fax : 04-76-57-49-81
Conception d'un capteur de vibrations pour un système d'aide au monitoring per-opératoire dans la chirurgie de l'oreille moyenne / Vibration Sensor for per-operatory Monitoring during the Middle-ear Surgery
Equipe : MNS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Date de début : 2012
Durée : 4 à 6 mois
Profil : Consulter la fiche.
Personne à contacter : Libor RUFER et Skandar BASROUR
TIMA, 46 av
Félix Viallet 38031 Grenoble Cedex
Tél : 0476574306/07 ; Fax : 0476574981
Dispositifs à base des ondes acoustiques de surface pour un transport cohérent d’un spin électronique unique / SAW-based device for coherent transport of single electron spin
Equipe : MNS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Date de début : 2012
Durée : 4 à 6 mois
Profil : Consulter la fiche.
Personne à contacter : Libor RUFER
TIMA, 46 av
Félix Viallet 38031 Grenoble Cedex
e-mail : LiborRufer[AT]imag[DOT]fr
Tél : 0476574306; Fax : 0476574981
Trois sujets : Vérification de flot de contrôle sur un processeur NIOS II; Analyse de durées de vie dans des circuits numériques; Analyse de criticité des registres dans un microprocesseur Sparc
Equipe : ARIS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Date de début : Année 2011/2012
Profil : Consulter la fiche.
Personne à contacter : Régis LEVEUGLE
TIMA, 46 av Félix Viallet 38031 Grenoble Cedex
e-mail : RegisLeveugle[AT]imag[DOT]fr
Tél : 0476574686; Fax : 0476574981
Pré-chargement dans une hiérarchie mémoire
Equipe : SLS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Durée : 5 mois
Profil : Consulter la fiche.
Personne à contacter : Stephane Mancini
Optimisation de la gestion des données dans un flot de conception HLS
Equipe : SLS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Durée : 5 mois
Profil : Consulter la fiche.
Personne à contacter : Stephane Mancini
Master Internship: Assertion-Based Verification of hardware systems: generation of proper test sequences
Equipe : VDS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Date de début : beginning of 2012
Durée : 6 months
Profil : The design of leading-edge hardware/software devices (PDAs, smartphones, digital cameras,...) is a complex process that increasingly involves the use and interconnection of large components. Guaranteeing their correctness is a challenging issue. In this context, Assertion-Based Verification can be of great help to verify the correctness of the systems under development: it involves formal or semi-formal methods to check whether the system complies with its requirements or expected behaviour, formalized as logic and temporal assertions (written in languages such as the IEEE standards PSL or SVA).
Various solutions exist for the construction of property checkers (monitors) from temporal assertions. Such property checkers are connected to the design under verification and inform about the satisfaction of the properties during simulation or FPGA emulation. In this process, guaranteeing that the property is not verified vacuously is crucial. Test sequences cannot be generated purely randomly: they must be designed to ensure a good coverage of the monitor's activation conditions. Consider as a trivial example a property of the form always(A implies B), which means that it is always true that, if A holds, then B also holds. If the testbench is such that A never holds, then the property is always verified, but verified vacuously i.e., without having actually been checked. In general, the form of the property can be more complex, and the Boolean sub-expressions involved in the temporal assertion (such as A and B in the example) can be expressions over the device primary inputs but also over its internal state and primary outputs. Thus, determining test sequences for the primary inputs that can ensure non vacuity does not have a straightforward solution.
The goal of the internship will be to take part in the research work of the VDS team of the TIMA Laboratory in this area. The team works towards the development of a specific method for the automatic test sequences generation directed by the necessity to avoid vacuous assertion satisfaction. The intern will have to: learn some notions related to hardware verification and more precisely to assertion-based verification, make a state of the art of research in coverage analysis, generation of test sequences related to temporal properties, etc..., and contribute to the development, implementation and test of algorithms for solving the problem described above.
Required skills:
* good basis of logics,
* good basis of hardware architecture,
* knowledge in hardware verification and/or specification languages like PSL would be a plus.
Personne à contacter :
Prof Laurence PIERRE
TIMA Laboratory
Tel +33 (0)4 76 57 49 92
laurencepierre[AT]imag[DOT]fr
Gestionnaire de composants matériels sur architecture dynamiquement reconfigurable
Equipe : SLS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Date de début : printemps 2012
Durée : 5 à 6 mois
Profil : Consulter la fiche.
Personne à contacter : Olivier Muller , Yan Xu
