Proposal for Phd Thesis : "Eliminating Useless Transitions in Sequential Circuits"


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.


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:

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:

  1. Knowledge in the basics of computer science and digital circuits design: Boolean functions, automata and formal languages, algorithms, complexity, compilation, formal verification;
  2. Good programming skills.
Knowledge of French is advantageous but does not constitute a pre-requisite.



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 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.


Oded Maler, CNRS-Verimag
Fahim Rahim, Atrenta Ltd