With the widespread use of small mobile computing devices like smartphones and tablets, power efficiency has become a very important design criterion for hardware manufacturers like Intel, AMD, Infineon, ST, Qualcom, Nvidia, etc. This is due to the limited energy storage capacity of mobile devices, imposed by constraints on their size and weight, as well as by problems of heat dissipation. Similar considerations of power efficiency apply to implanted medical devices, wearable computing, UAV (unmanned airborne vehicles), satellites and sensor networks.
Since chip design has become more and more automated, electronic design automation companies consider energy efficiency as a prime concern in circuit design. However, so far, there has been hardly any use of formal mathematical methods in energy efficient circuit design. Instead, the main techniques used in practice were either based on simulation or on semi-formal approaches reasoning about patterns and structural properties. Typical work areas are the following:
1. Power estimation (based on simulation),
2. Power verification (of structural (i.e., non-dynamic) properties),
3. Power optimisation (coarse high-level reasoning about size and structural patterns), and
4. Formal power verification (model checking applied to coarse abstractions based on activation/deactivation of blocks on the chip).
In this project, we bring modern formal mathematical methods into automated circuit design. This yields a new domain of
"5. Formal power optimisation".
Here, efficient circuit design is achieved via solving the controller synthesis problem. This is to construct a controller that achieves (in every context) a combination of several objectives:
(a) the functional correctness of the induced behaviour, as specified in the requirements specification,
(b) a guaranteed limit on the peak energy consumption (i.e., an upper bound on the worst case), and
(c) a low average energy consumption.
While (a) and (b) are absolute constraints, the relative quality of the controller is measured in terms of how well it achieves objective (c).
We solve the synthesis problem by applying modern mathematical techniques and tools from game theory (energy games, mean-payoff games), formal software verification (formal requirements specification and automata), and logic and algorithms (SAT and SMT solvers). Beyond theoretical advances and new techniques for the synthesis of energy efficient controllers, the project aims for practical application of controller synthesis in the new field of Formal Power Optimisation in circuit design. A prototype of a software tool that implements the new methods and applies them to power optimization in chip design will be evaluated on case studies provided by our industrial project partner Atrenta Inc.
|