Background:
The problem of reducing power consumption in computers in general and in mobile devices in particular is a major problem in contemporary system design. For mobile devices such as smart phones, reducing consumption increases battery life and autonomy. The energy consumption of a processor is related to the number of gate switchings that it performs. It had been observed that many of these transitions are redundant and do not influence the logical behavior of the machine. To understand why these useless transitions have been introduced in the first place one should look more closely at the design process.
A microprocessor is essentially a sequential machine, a finite-state automaton with a huge number of binary inputs and state variables. It is realized by a network of Boolean gates and memory elements. Modern processors are not written directly using these terms but are written first in what is called RTL (register transfer level) which is a higher level language with variables that correspond to registers. From there an abstract sequential machine is derived and realized using logical building blocks (synthesis). There are many degrees of freedom in this process and each choice leads to a circuit of different size and a different realization of the next-state logic that may optimize different criteria (size, speed). It turns out that the output of contemporary synthesis tools exhibits such redundant transitions.
Goals:
The goal of the thesis is to find methods to identify transition redundancy in synthesized circuits as a first step toward transforming them into circuit which are logically equivalent but energetically more efficient. The work is roughly divided into two parts:
- Theoretical foundations (supervised in Verimag): study the problem of minimizing finite-state machine (automata) at the micro-level, that is, when one considers the encoding of input symbols and states using a huge number of Boolean variables. Develop algorithms for minimization and semantics preserving transformations on such automata;
- Application (supervised in Atrenta): apply the techniques developed in the first part to real designs by Atrenta clients and make first steps to integrate them in a commercial tool chain.
Administrative Aspects:
The thesis will be part of the French CIFRE program (pending approval) where the candidate is employed for 3-years by the company with a competitive salary. The candidate will spend his/her time evenly between Verimag and Atrenta, depending on the relative intensity of theoretical and practical work at each period. The PhD title will be from the University of Grenoble in computer science (informatique).
Candidate Quality:
We are looking for motivated candidates with good theoretical as well as practical skills. The following qualifications are important:
- Knowledge in the basics of computer science and digital circuits design: Boolean functions, automata and formal languages, algorithms, complexity, compilation, formal verification;
- Good programming skills.
Timeline:
- 30/5 - 15/6/11: Send application (CV + motivation letter) to Oded.Maler@imag.fr and fahim@atrenta.com
- 15/6 - 30/6: Interviews with selected candidates
- Early July: Decisions / contract signature
- 15/9/11: Start of work
VERIMAG:
Verimag is one of the leading academic labs in verification and model-based design of embedded systems. Its past contributions include model checking (J. Sifakis, Turing Award 2007), the data-flow language Lustre (P. Caspi, N. Halbwachs) underlying the SCADE programming environment for safety-critical systems, as well as pioneering contributions to the study of timed and hybrid systems.
ATRENTA:
Atrenta is one of the largest private electronic design automation companies with over 170 customers, including 18 of the top 20 semiconductor and consumer electronics companies. Through its SpyGlass(r) and GenSys(r) products, Atrenta provides SoC (System on Chip) realization solutions that improves the process of going from design to fabrication. These tools deliver higher quality chips, predictable design coherence, automated chip assembly and improved implementation readiness. Atrenta's GuideWare reference methodologies open the way for broader deployment of system on chip (SoC) devices in the marketplace, improving time to market, reducing implementation costs and lowering risk. The work will be conducted in the recently opened R&D center of Atrenta in Grenoble.
Contacts:
Oded Maler, CNRS-Verimag
Fahim Rahim, Atrenta Ltd