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.