Property First Hardware Design - A Correct-by-Construction Methodology for RTL Design from System Level Models

在过去的几十年里，摩尔定律充分地描述了微电子和纳米电子工业的技术进步。它正确地预测了在可承受的成本下，每1.8年可以集成在单个芯片上的晶体管数量就会重复一次。然而，与此同时，很明显，这一发展已经大大放缓，并将在未来进一步放缓，对微电子工业产生深远的影响：虽然在过去，从一个技术过程节点到下一个技术过程节点的周期性迁移一直是触发创新的成功秘诀，但未来微电子产品的增强将越来越依赖于使用结合了新的强大优化技术的新设计方法来设计先进的微架构。另一方面，积极优化的设计容易出错，需要特别强大的验证方法。电子系统设计联盟报告说，在过去的一年中，正式验证技术的使用增加了两倍。这证明了一个事实，即随着摩尔定律的终结，芯片系统（SoC）硬件的创新设计和验证方法正在重新引起人们的兴趣。该研究项目将探索和开发一种全新的SoC硬件设计方法，以满足未来的需求。所研究的方法学将采用将正式验证技术集成到设计流程中的新概念。特别地，它将利用形式抽象技术的最新成果，从系统级模型开始，在寄存器传输级（RTL）系统地创建可证明正确的硬件设计。新的方法不仅要减少设计和验证的工作量。通过早期将形式化方法集成到设计过程中，设计人员将受益于关于设计组件之间的逻辑和时间关系的全面和详细的知识，并可以使用这些知识对微架构进行高级优化。特别是，该项目的目标是展示如何利用迄今为止未使用的优化潜力来降低SoC功耗。所提出的方法不需要其用户在正式SoC验证方面的任何高级知识。它没有对可能的设计改进施加任何限制。相反，它通过额外的措施补充和扩展了今天大多数手工设计实践。它们确保RTL设计作为系统模型的精化的正确性，并在RTL对象和系统级描述之间建立正式的联系。因此，系统的详细行为以一种可理解的方式被记录下来，并且可以有效地用于优化。

In the past, over several decades Moore's famous law adequately described the technological progress in the micro- and nanoelectronics industry. It correctly predicted a duplication every 1.8 years in the number of transistors that can be integrated on a single chip under affordable costs. Meanwhile, however, it has become apparent that this development has slowed down substantially and will slow down even more in the future, with far-reaching consequences for the microelectronic industry: while, in the past, periodical migration from one technological process node to the next kept being a successful recipe to trigger innovation, future product enhancements in microelectronics will rely increasingly on designing advanced microarchitectures using new design methodologies that incorporate new and powerful optimization techniques. Aggressively optimized designs, on the other hand, are prone to errors and call for particularly powerful verification methods. The Electronic System Design Alliance reports that the use of formal verification techniques in the past year has increased by a factor of two. This attests to the fact that, with the end of Moore's Law, innovative design and verification methods for System-on-Chip (SoC) hardware are receiving a lot of renewed interest. This research project will explore and develop a fundamentally new methodology for the design of SoC hardware that shall meet the future requirements. The investigated methodology will employ new concepts of integrating formal verification techniques into the design flow. In particular, it will leverage recent results on formal abstraction techniques to systematically create provably correct hardware designs at the Register Transfer Level (RTL) starting from system level models. The new methodology shall not only reduce the efforts for design and verification. By early integration of formal methods into the design process the designer will benefit from comprehensive and in-detail knowledge about logic and temporal relationships between design components and can use this knowledge for advanced optimizations of the microarchitecture. In particular, it is a goal of this project to demonstrate how so-far unused optimization potential for reducing SoC power consumption can be exploited. The proposed methodology does not require any advanced knowledge in formal SoC verification from its users. It neither imposes any restrictions with respect to possible design refinements. Instead it supplements and extends today's mostly manual design practices by additional measures. They ensure the correctness of the RTL design as a refinement of the system model and establish a formal link between the RTL objects and the system level description. As a result, the detailed behavior of the system is documented in a comprehensible way and can be exploited effectively for optimization.