- Rolf Drechsler, University of Bremen, Germany
Title: Coverage at the Formal Specification Level
Authors: Rolf Drechsler, Julia Seiter, Mathias Soeken
Formal verification is a powerful and effective method to ensure correctness of electronic systems. In order to check whether enough properties have been written coverage metrics have been proposed along with methods to automatically increase the coverage by determining new properties for missed scenarios. In the invited talk we present how such coverage methods can be leveraged to higher levels in the design flow of electronic systems. We first review existing coverage metrics and demonstrate state-of-the art formal verification techniques for correctness checking at the Formal Specification Level (FSL). Based on those we describe how coverage techniques can help to automatically derive missed scenarios at the FSL, where structure and behavior are given in terms of UML class and sequence diagrams, respectively.
Rolf Drechsler received the Diploma and Dr. Phil. Nat. degrees in computer science from J.W. Goethe University Frankfurt am Main, Frankfurt am Main, Germany, in 1992 and 1995, respectively. He was with the Institute of Computer Science, Albert-Ludwigs University, Freiburg im Breisgau, Germany, from 1995 to 2000, and with the Corporate Technology Department, Siemens AG, Munich, Germany, from 2000 to 2001. Since October 2001, he has been with the University of Bremen, Bremen, Germany, where he is currently a Full Professor and the Head of the Group for Computer Architecture, Institute of Computer Science. In 2011, he additionally became the Director of the Cyber-Physical Systems group at the German Research Center for Artificial Intelligence (DFKI) in Bremen. His current research interests include the development and design of data structures and algorithms with a focus on circuit and system design.
Rolf Drechsler was a member of Program Committees of numerous conferences including e.g., DAC, ICCAD, DATE, ASP-DAC, FDL, MEMOCODE, FMCAD, Symposiums Chair ISMVL 1999 and 2014, and the Topic Chair for “Formal Verification” DATE 2004, DATE 2005, DAC 2010, as well as DAC 2011. He is a co-founder of the Graduate School of Embedded Systems and he is the coordinator of the Graduate School “System Design” funded within the German Excellence Initiative. He received best paper awards at the Haifa Verification Conference (HVC) in 2006, the Forum on specification & Design Languages (FDL) in 2007 and 2010, the IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS) in 2010 and the IEEE/ACM International Conference on Computer-Aided Design (ICCAD) in 2013.
- Wolfgang Kunz, University of Kaiserslautern, Germany
Title: The big hurdles for FV tools in industrial practice – can we overcome them insystem-level design flows?
Dept. of Electrical and Computer Engineering
Technische Universität Kaiserslautern, Germany
Decades of research in the field of formal verification have resulted in a number of break-through successes. In many applications, the scalability of formal techniques no longer causes concern. Adequate specification languages such as PSL and SVA have been developed that match well with powerful proof algorithms. Standardization of these languages has facilitated their adoption in industry. Moreover, sophisticated methodologies have emerged in industry that proved to be highly productive. Yet, when deploying tools and methodologies for formal verification in industrial practice a number of hurdles have to be faced. Only fully automatic techniques such as equivalence checking and automatic linting enjoy wide-spread popularity in SoC design. Property checking, on the other hand, is only moderately successful. As a result, simulation has continued to be the predominant verification technique.
Based on observations of industrial practices over many years, this talk will identify a set of hurdles that impede formal techniques in gaining further ground oversimulation-based verification. After inspecting these hurdlesnew lines of research will be proposed for overcoming them. In particular, it will be argued that the future success of formal techniques may depend on how these techniques are integrated into system-level design flows. It is proposed to leverage existing formal technology as a contribution to close the “semantic gap” between the system level and the register-transfer level. This has a strong impact on how to use and design formal verification tools both for hardware and for low-level software. The talk will describe recent results and new practices already explored in industrial case studies. In conclusion, a new system design methodology including formal techniques is envisioned to support effective design procedures based on high-level synthesis as well as manual design refinements at the system level.
Wolfgang Kunz received the Dipl.-Ing. degree in Electrical Engineering from the University of Karlsruhe, Germany, in 1989 and the Dr.-Ing. degree in Electrical Engineering from the University of Hannover, Germany, in 1992.
From 1993 to 1998, he was with Max Planck Society, Fault-Tolerant Computing Group at the University of Potsdam, Germany. From 1998 to 2001 he was a professor of Computer Science at the University of Frankfurt/Main. Since 2001 he is a professorat the Department of Electrical & Computer Engineering at Technische Universität Kaiserslautern.
Wolfgang Kunz conducts research in the area of System-on-Chip design and verification collaborating with several industrial partners including AbsInt, Alcatel-Lucent, Atrenta, Audi, Bosch, Infineon and OneSpin Solutions.
For his research activities Wolfgang Kunz has received several awards including the Berlin Brandenburg Academy of Science Award and the Award of the German IT Society. Wolfgang Kunz is a Fellow of the IEEE.
- Fahim Rahim, Atrenta, France
Title: Efficiently using formal verification techniques to reduce power
Atrenta's Spyglass Power Platform allows the designer to reduce SoC power at the RT level. Spyglass detects fine-grain power saving opportunities to reduce register and memory power consumption and automatically modifies the original RTL to include the newly identified power saving opportunities. In addition, the tool detects potential coarse grain power optimization in the SoC and guide the designer to explore power consumption of their SoC Spyglass employs formal verification techniques to explore the design space for power saving opportunities and prove that the proposed opportunities don't modify the design functionality. The talk will illustrate how formal verification techniques are being used to drive Spyglass technology and outline future challenges in the field of power reduction.
Fahim Rahim is the managing director of Atrenta in Europe and has over 20 years of experience in the field of Electronic Design Automation and has worked on all aspects of synthesis, ESL design, and formal verification. He holds a PhD in Formal Verification from the University of Paris (UPMC) and is the author of over 10 conference papers and journal articles presented at IEEE Conferences. He has previously worked as a senior researcher at the Synopsys Advanced Research Lab, California, and was one of the early members of Mentor Graphics Advanced Research Lab