EPSRC logo

Details of Grant 

EPSRC Reference: EP/M027287/1
Title: Energy Efficient Control
Principal Investigator: Schewe, Professor S
Other Investigators:
Wojtczak, Dr DK
Researcher Co-Investigators:
Project Partners:
Atrenta Inc (International)
Department: Computer Science
Organisation: University of Liverpool
Scheme: Standard Research
Starts: 01 September 2015 Ends: 31 March 2019 Value (£): 429,107
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
EP/M027651/1
Panel History:
Panel DatePanel NameOutcome
14 Apr 2015 EPSRC ICT Prioritisation Panel - Apr 2015 Announced
Summary on Grant Application Form
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.

Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Summary
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.liv.ac.uk