TIMA (Techniques of Informatics and Microelectronics
for integrated systems Architecture) is a public research Laboratory, affiliated with
the Scientific Universities of Grenoble (Grenoble INP, UJF) and the French CNRS. TIMA has
two decades of experience in hardware design, hardware-dependent software, MEMS, and CAD.
With about 100 academic researchers and PhD students from over 25 nationalities, TIMA
is leading international level research, in close cooperation with academic and industrial
partners in Europe and in the world. Most of the activities are performed in the context
of partnerships, with an emphasis on European and national cooperative projects.
TIMA is structured into six research groups, whose current activities focus on: reliability,
robustness and fault tolerance for complex integrated systems (ARIS), design and tools for
asynchronous circuits/systems and non-uniform sampling and processing (CIS), design,
technologies and power scavenging for autonomous micro and nano systems (MNS), design and
test of mixed-signal systems (RMS), hardware and software architectures, design and CAD
tools for MPSOC's and NOC-based heterogeneous systems (SLS), formal methods for the
specification, validation and debug of complex systems (VDS). TIMA researchers take an
active part in the organization of successful international conferences and schools,
some of which they initiated. Seven spin-off companies were created to industrialize and
distribute TIMA's research results.
Contribution to the SoCKET project
The VDS and ARIS groups contribute to the SoCKET project, in the activities related to
formal and semi-formal verification and robustness analysis.
Formal and semi-formal verification provide a reliable approach to guarantee the correctness
of circuits being designed. In that framework, the expected behaviour (specification) is
described using a mathematical model, and formal or semi-formal reasoning is applied. It
usually amounts to verifying either the functional correctness of the system or the validity
of temporal properties. The TIMA expertise in this area covers the application of theorem provers
to the formal verification of various categories of circuits, as well as the formal verification
using model-checking techniques, and also the development of semi-formal methods devoted to
the runtime verification of temporal properties using synthesizable monitors.
Designing dependable circuits requires in particular evaluating, at each step in the design flow,
the achieved level of robustness against various types of faults or errors. Errors are generally
the consequence of natural phenomena such as particle impacts, electromagnetic perturbations,
electrical noise or degradations due to aging. Robustness evaluation requires a wide expertise
in the analysis of the functional effects of error propagations, from the early stages of the
design flow up to the electrical-level or even physical-level descriptions. Complementary
techniques are necessary. Such a multi-level expertise is available at TIMA, where various
methods have already been developed. The evaluation could also be complemented by hardening
techniques, integrated in highly critical systems.
This expertise will be applied to the case studies proposed by the industrial partners.
TIMA takes part in all the sub-projects of the SoCKET project. It is
leader of sub-project 6 (dissemination of results).
