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.

Potential Impact:
The impact of this research will first be felt by chip manufacturers and the service industry around them. The techniques we develop will allow for energy efficient solutions that increase the time applications and appliances depending on batteries will work independently of external energy supply. This is particularly important for light appliances like mobile phones.

Besides improving the quality of the product (chip) produced, the techniques we will develop allow for a separation of concerns during the development process. Instead of requiring the system developer to improve energy efficiency herself, this task is automated, leading to a leaner, cheaper, and faster development process.

In a next step, the techniques we develop will serve a wider share of engineering and IT industry. Once established, the automated development of optimal control is not bound to the application of chip design, and more optimisation criteria than energy efficiency can be tackled. This will allow for adjusting the developed techniques, e.g., in robotic, or health care systems.

More applications that benefit from increased energy efficiency include pace makers with a longer life span and lighter satellites that can use smaller solar panels. Applications that benefit from optimisation against other objective functions are controllers that lead to better load balancing and optimising the access control strategy for resources that cannot be shared.

A further advantage of applying the techniques that we will develop is that it brings formal techniques into use in an early stage of system development. This prepares the ground for a more thorough coverage of the design process by formal correctness analysis, which in turn will lead to an increased reliability of the systems produced.

These advantages will serve the UK industries involved in the first instance, but they will also serve the public. The customers will benefit from the higher quality of the products, such as mobile phones with increased lifetime. Patients will benefit from longer battery life in pace makers, and services that use satellites can be offered at lower prices if their energy efficiency (and thus their weight) is reduced.