Energy Efficient Control
Lead Research Organisation:
University of Liverpool
Department Name: Computer Science
Abstract
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.
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.
Planned 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.
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.
Publications
Apt KR
(2015)
Coordination Games on Directed Graphs
Hahn E M
(2015)
Lazy Probabilistic Model Checking without Determinisation
Gupta A
(2015)
Incentive Stackelberg Mean-payoff Games
Gupta A
(2015)
Making the Best of Limited Memory in Multi-Player Discounted Sum Games
in Electronic Proceedings in Theoretical Computer Science
Brook A
(2015)
Local and global fairness in concurrent systems
Apt K
(2016)
Logics in Artificial Intelligence
Huang C
(2016)
Model-checking iterated games
in Acta Informatica
Fearnley J
(2016)
Efficient approximation of optimal control for continuous-time Markov games
in Information and Computation
Husien I
(2016)
Software Engineering and Formal Methods
Description | We have developed techniques that take Energy consumption into account when synthesising control strategies. The techniques we have developed reach from pure theory, where Energy is considered to be limited resource, to practical approaches that construct controls for systems on chips. |
Exploitation Route | As techniques from an emerging field, there is a lot of room for extensions and improvement. Other groups could work on improving the efficiency or effectiveness of our techniques, or complement them with alternative ways to obtain similar goals. |
Sectors | Digital/Communication/Information Technologies (including Software),Electronics,Energy |
Description | (FOCETA) - FOUNDATIONS FOR CONTINUOUS ENGINEERING OF TRUSTWORTHY AUTONOMY |
Amount | € 4,985,540 (EUR) |
Funding ID | 956123 |
Organisation | European Commission |
Sector | Public |
Country | European Union (EU) |
Start | 10/2020 |
End | 09/2023 |
Description | (PaVeCo) - Parametrised Verification and Control |
Amount | € 195,455 (EUR) |
Funding ID | 753351 |
Organisation | European Commission |
Sector | Public |
Country | European Union (EU) |
Start | 11/2017 |
End | 10/2019 |
Title | ReaTK: Reactive System Verification and Synthesis ToolKit |
Description | ReaTK is the Reactive System Verification and Synthesis ToolKit. It provides the ReaVer tool dedicated to the static verification of logico-numerical systems by abstract interpretation, and the ReaX tool performing discrete controller synthesis for such systems. ReaX implements various algorithms for synthesizing controllers that target safety objectives, reachability objectives (an "easy" subclass of liveness properties), as well as numerical optimization objectives. Fulfilling the latter class of objectives consists in controlling the system so that value of a cost function expressed on its variables is minimized over a specified time interval. ReaX implements various algorithms that handle such objectives on sliding windows, or with discounted costs (not published yet). Controllers synthesized with ReaX are always implementable, which means that they can easily be translated into efficient sequential code, or alternatively, into hardware circuits. |
Type Of Technology | Software |
Year Produced | 2014 |
Open Source License? | Yes |
Impact | ReaX is the first controller synthesis tool that is able to handle infinite-state systems for safety objectives. As such, it has been used by multiple researchers, especially in the Discrete Events Systems research community. ReaX is also involved for the compilation of the Heptagon/BZR synchronous language (http://heptagon.gforge.inria.fr/), where controller synthesis is used to enforce contracts. As such, it is regularly used as part of the teaching curriculum of Masters' lectures. ReaX was also involved recently for the development of a program analysis tool for verifying and enforcing security properties (such as data integrity and confidentiality). |
URL | http://reatk.gforge.inria.fr |