Energy Efficient Control

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

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.