Employment at TIMA
Internship proposals
Intégration d’un composant mémoire multi-ports dans un outil de synthèse d’architecture
Host: SLS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Start Date: printemps 2012
Duration: 5 à 6 mois
Profile: Consulter la fiche.
Contact person: Olivier Muller, Adrien Prost-Boucle et Frédéric Rousseau
Modélisation haut niveau d’un capteur de vision CMOS sur SystemC-AMS
Host: CIS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Start Date: 2012
Profile: Consulter la fiche.
Contact person: 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
Host: CIS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Start Date: 2012
Profile: Consulter la fiche.
Contact person: 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
Host: MNS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Start Date: 2012
Duration: 4 à 6 mois
Profile: Consulter la fiche.
Contact person: Libor RUFER et Skandar BASROUR
TIMA, 46 av
Félix Viallet 38031 Grenoble Cedex
Tél : 04
76
57
43
06/07 ; Fax : 04
76
57
49
81
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
Host: MNS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Start Date: 2012
Duration: 4 à 6 mois
Profile: Consulter la fiche.
Contact person: Libor RUFER
TIMA, 46 av
Félix Viallet 38031 Grenoble Cedex
e-mail : Libor
Rufer[AT]imag[DOT]fr
Tél : 04
76
57
43
06; Fax : 04
76
57
49
81
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
Host: ARIS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Start Date: Année 2011/2012
Profile: Consulter la fiche.
Contact person: Régis LEVEUGLE
TIMA, 46 av
Félix Viallet 38031 Grenoble Cedex
e-mail : Regis
Leveugle[AT]imag[DOT]fr
Tél : 04
76
57
46
86; Fax : 04
76
57
49
81
Pré-chargement dans une hiérarchie mémoire
Host: SLS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Duration: 5 mois
Profile: Consulter la fiche.
Contact person: Stephane Mancini
Optimisation de la gestion des données dans un flot de conception HLS
Host: SLS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Duration: 5 mois
Profile: Consulter la fiche.
Contact person: Stephane Mancini
Master Internship: Assertion-Based Verification of hardware systems: generation of proper test sequences
Host: VDS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Start Date: beginning of 2012
Duration: 6 months
Profile: 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.
Contact person:
Prof
Laurence PIERRE
TIMA Laboratory
Tel
+33 (0)4 76 57 49 92
laurence
pierre[AT]imag[DOT]fr
Gestionnaire de composants matériels sur architecture dynamiquement reconfigurable
Host: SLS-TIMA, 46 Avenue Félix Viallet, 38031 Grenoble Cedex
Start Date: printemps 2012
Duration: 5 à 6 mois
Profile: Consulter la fiche.
Contact person: Olivier Muller , Yan Xu


