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

• Applicant: Professor Dr.-Ing. Wolfgang Kunz
• Subject Area: Computer Architecture, Embedded and Massively Parallel Systems ; Security and Dependability, Operating-, Communication- and Distributed Systems
• Term: from 2016 to 2021
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 328724410

• Final Report Year: 2021

Final Report Abstract

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 has explored and developed a fundamentally new methodology for the design of SoC hardware that shall meet the future requirements. A new methodology was developed to integrate formal verification techniques into the design flow. In particular, it leverages formal abstraction techniques to systematically create provably correct hardware designs at the Register Transfer Level (RTL) starting from system-level models. The benefits of the new methodology have been examined at the example of several case studies. It was shown that transaction-level models of industrial relevance can be put into a formal relationship with their RTL implementation, thus, closing the semantic gap between both levels. This opens new opportunities to shift design and verification tasks from the RTL to the system level, which has been shown to significantly reduce manual efforts. By early integration of formal methods into the design process the designer benefits 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, this project has demonstrated how to use this knowledge in safety analysis and to exploit so far unused optimization potential for SoC power consumption. Specifically, several case studies showed that the new approach leads to power savings by clock gating of up to 56 % (avg. 22%), on top of the power savings reached by a state-of-the-art commercial tool. The new techniques for power gating contributed additional power savings of up to 21 % (avg. 15%). 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. Two scientists funded by this project explore commercialization of the research results under a grant from the program “EXIST – Existenzgründungen aus der Wissenschaft”.

Publications

• “Dynamic power optimization based on formal property checking of operations,” in 20. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Bremen, Germany, 2017
  S. Udupi, J. Urdahl, D. Stoffel, and W. Kunz
  
• “Dynamic power optimization based on formal property checking of operations,” in Proc. Intl. Conf. on VLSI Design (VLSID), 2017
  S. Udupi, J. Urdahl, D. Stoffel, and W. Kunz
  
• “Exploiting hardware unobservability for lowpower design and safety analysis in formal verification-driven design flows,” IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol. 27, no. 6, pp. 1262–1275, June 2019
  S. Udupi, J. Urdahl, D. Stoffel, and W. Kunz
  
• “Property-driven development of a RISC-V CPU,” in Proc. Design and Verification Conference United States (DVCON-US), 2019
  T. Ludwig, M. Schwarz, J. Urdahl, L. Deutschmann, S. Hetalani, D. Stoffel, and W. Kunz
  
• “Properties first – correct-by-construction RTL design in system-level design flows,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 39, pp. 3093–3106, June 2020
  T. Ludwig, J. Urdahl, D. Stoffel, and W. Kunz