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

点击翻译按钮获取中文摘要

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.