Energy Efficient Control

节能控制

• 批准号: EP/M027287/1
• 负责人: Sven Schewe
• 金额: $ 54.68万
• 依托单位: University of Liverpool
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2015
• 资助国家: 英国
• 起止时间: 2015 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FM027287%2F1
• 关键词: Energy; Efficient; Control

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), and4. 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.

随着智能手机和平板电脑等小型移动的计算设备的广泛使用，功率效率已成为英特尔、AMD、英飞凌、ST、Qualcom、Nvidia等硬件制造商的一个非常重要的设计标准。这是由于移动的设备的能量存储容量有限，这是由其尺寸和重量的约束以及散热问题造成的。类似的能效考虑也适用于植入式医疗设备、可穿戴计算、无人机（UAV）、卫星和传感器网络。由于芯片设计越来越自动化，电子设计自动化公司将能效视为电路设计的首要考虑因素。然而，到目前为止，在节能电路设计中几乎没有使用任何形式的数学方法。相反，在实践中使用的主要技术是基于模拟或半正式的方法推理模式和结构特性。典型的工作领域如下：1.功率估计（基于模拟），2。功率验证（结构（即，非动态）特性），3.功率优化（关于大小和结构模式的粗略高级推理），以及4。形式化电源验证（基于芯片上模块的激活/去激活应用于粗略抽象的模型检查）。在这个项目中，我们将现代形式化数学方法引入自动化电路设计。这将产生一个新的域“5。这里，通过解决控制器综合问题来实现有效的电路设计。这是为了构造一种控制器，该控制器实现（在每个上下文中）几个目标的组合：（a）如在需求规范中指定的，诱导行为的功能正确性，（B）峰值能耗的保证限制（即，虽然（a）和（B）是绝对约束，但控制器的相对质量是根据它实现目标（c）的程度来测量的。我们解决的综合问题，应用现代数学技术和工具，从博弈论（能源游戏，平均收益游戏），正式的软件验证（正式的需求规格说明和自动机），逻辑和算法（SAT和SMT求解器）。除了理论上的进步和新技术的节能控制器的合成，该项目的目的是控制器合成的实际应用在电路设计中的形式功率优化的新领域。一个软件工具的原型，实现了新的方法，并将其应用到芯片设计中的功率优化，将在我们的工业项目合作伙伴Atrenta公司提供的案例研究进行评估。

项目成果

Coordination Games on Weighted Directed Graphs

加权有向图上的协调博弈

• DOI: 10.1287/moor.2021.1159
• 发表时间: 2022
• 期刊: Mathematics of Operations Research
• 影响因子: 1.7
• 作者: Apt K

Coordination Games on Directed Graphs

有向图上的协调博弈

• 发表时间: 2015
• 作者: Apt KR

Verification of Distributed Epistemic Gossip Protocols

分布式认知八卦协议的验证

• DOI: 10.1613/jair.1.11204
• 发表时间: 2018
• 期刊: Journal of Artificial Intelligence Research
• 影响因子: 5
• 作者: Apt K

Logics in Artificial Intelligence

人工智能中的逻辑

• DOI: 10.1007/978-3-319-48758-8_2
• 发表时间: 2016
• 作者: Apt K

Common Knowledge in a Logic of Gossips

八卦逻辑中的常识

• DOI: 10.4204/eptcs.251.2
• 发表时间: 2017
• 期刊: Electronic Proceedings in Theoretical Computer Science
• 作者: Apt K