Title
Energy Efficient Control

CoPED ID
c0369c2d-4524-4a9f-83f9-f774bb69ffe5

Status
Closed

Funders

Value
£742,794

Start Date
Aug. 31, 2015

End Date
Aug. 30, 2019

Description

More Like This


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.

Richard Mayr PI_PER

Subjects by relevance
  1. Optimisation
  2. Planning and design
  3. Energy efficiency
  4. Programming
  5. Mobile devices
  6. Microcircuits
  7. Design (artistic creation)
  8. Tablet computers
  9. Simulation
  10. Energy
  11. Modelling (creation related to information)
  12. Verification
  13. Electronic circuits
  14. Software design
  15. Smartphones

Extracted key phrases
  1. Energy Efficient Control
  2. Small mobile computing device
  3. Energy efficient circuit design
  4. Widespread use
  5. Formal power verification
  6. Formal power optimisation&quot
  7. Mobile device
  8. Modern formal mathematical method
  9. Important design criterion
  10. Power efficiency
  11. Electronic design automation company
  12. Chip design
  13. Limited energy storage capacity
  14. Energy efficiency
  15. Controller synthesis problem

Related Pages

UKRI project entry

UK Project Locations
1 km
Leaflet | © OpenStreetMap contributors