Wolfgang Kunz - Publications#
Publications older than 5 years:
[1] Wolfgang Kunz: "HANNIBAL: an efficient tool for logic verification based on recursive learning", IEEE/ACM International Conference on Computer-Aided Design (ICCAD), 1993.
Summary: The paper presents one of the very first industry-strength methods for formal equivalence checking.
Impact: > 160 citations. The method was adopted in one of the first commercial equivalence checkers, commercialized by Mentor Graphics. Today, formal equivalence checking using the same or similar principles, as described in this paper, is employed world-wide in nearly all System-on-Chip design flows. Together with no more than two other research groups, Prof. Kunz is recognized as an inventor of this technique.
[2] Wolfgang Kunz, Dhiraj K. Pradhan: "Recursive learning: a new implication technique for efficient solutions to CAD problems - test, verification, and optimization", IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, 13(9), 1994.
Summary: The paper presents a fundamentally new reasoning algorithm for Boolean logic circuits.
Impact: > 300 citations. This reasoning algorithm has been used in tools for Electronic Design Automation worldwide. For example, Synopsys Design Compiler, the market-leading tool for circuit synthesis, adopted this approach for circuit optimization, as is known from talks by Synopsys representatives on several conference events.
[3] Oliver Wienand, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, Gert-Martin Greuel: "An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths", Computer-Aided Verification (CAV) 2008.
Summary: This paper makes the basic and interdisciplinary contribution of how to model logic-level circuits by Gröbner bases without the need of the computationally expensive Buchberger algorithm.
Impact: > 65 citations. This paper creates an important interdisciplinary link between the field of Logic Circuit Design and Computer Algebra.
[4] Minh D. Nguyen, Max Thalmaier, Markus Wedler, Jörg Bormann, Dominik Stoffel, Wolfgang Kunz: "Unbounded Protocol Compliance Verification Using Interval Property Checking With Invariants", IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, 27(11): 2068-2082, 2008.
Summary: This paper presents a new methodology and new algorithms for systematic System-on-Chip verification.
Impact: >75 citations. Contributions of this paper constitute the founding idea of OneSpin Solutions (https://www.onespin.com/) and were already commercialized several years before disclosing them in this paper. Founding staff of OneSpin Solutions, Jörg Bormann and Raik Brinkmann, now CEO of OneSpin Solutions, received their Ph.D. degree at TU Kaiserslautern under supervision of Prof. Kunz, with dissertations related to the topics of this paper. OneSpin Solutions has grown by 20% in each of the last 6 years, employs more than 60 people and is currently being acquired by Siemens EDA.
Recent Publications:
[5] M. Ammar Ben Khadra, Dominik Stoffel, Wolfgang Kunz: “Speculative disassembly of binary code”, International Conference on Compilers, Architectures, and Synthesis for Embedded Systems (CASES), 2016.
Summary: This paper proposes a reverse engineering technique for binary software code, a topic of high relevance, for example, in cybersecurity.
Impact: For the first time Control Flow Graph (CFG)-based function identification is proposed. The proposed approach significantly outperforms the leading industry disassembler IDA Pro and was adopted in the widely used commercial tool for reverse engineering and decompilation, Binary Ninja, https://binary.ninja/. Although open-source support was discontinued after graduation of the first author, the tool has attracted 87 stars on GitHub so far.
[6] Mohammad Rahmani Fadiheh, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra, Wolfgang Kunz: "Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking". Design Automation and Test in Europe (DATE-19), 2019.
Summary: This paper addresses the famous Spectre and Meltdown security vulnerabilities in processors and describes the first formal verification approach to detect such “Transient Execution Side Channels” in designs of realistic size.
Impact: To date, this is the only method which can exhaustively cover transient execution side channels at the concrete implementation level of processors. Work is under way at Siemens EDA (documented by mutual agreements) to commercialize this approach. After publication of this paper, Prof. Kunz received two research gifts from Intel Corp., USA, to further support this line of research and was invited to participate in Intel's Side Channel Academic Program (SCAP). SCAP is an Intel internal forum fostering collaboration in the field of security between Intel and selected academic groups world-wide.
The method published in this paper detected several so far unknown hardware vulnerabilities in processors, such as RISC-V Rocketchip and BOOM. These results have received attention also in science platforms, such as https://www.verdict.co.uk/chip-security-upec/, technical magazines, such as EETimes, https://www.eetimes.com/author.asp?section_id=36&doc_id=1334783, general news magazines, such as FOCUS news magazine, Germany, https://bit.ly/2ZpGrrA, as well as by the nation-wide public radio Deutschlandfunk, https://bit.ly/2KTpfmv.
[7] Tobias Ludwig, Joakim Urdahl, Dominik Stoffel, Wolfgang Kunz: ”Properties First - Correct-By-Construction RTL Design in System-Level Design Flows“, IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems 39(10): 3093-3106, 2020.
Summary: This paper proposes a solution to a fundamental problem in System-on-Chip design flows: High-level models of Systems-on-Chip are only considered prototypes and are created independently of the final designs. This paper shows how to create a formal relationship between high-level models and their lower-level implementations using a design procedure driven by formal methods. This ensures functionally correct design implementations and can lead to drastic improvements in industrial flows.
Impact: The ideas of this paper are commercialized in a TU Kaiserslautern spin-off, Lubis EDA, https://lubis-eda.com/. The first author of this paper received his Ph.D. under Prof. Kunz and is the CEO of LUBIS EDA. Already during the first year of its existence, LUBIS EDA has attracted a number of customers including Hyperstone, Dreamchip und iCHaus.
[8] Keerthikumara Devarajegowda, Mohammad Rahmani Fadiheh, Eshan Singh, Clark W. Barrett, Subhasish Mitra, Wolfgang Ecker, Dominik Stoffel, Wolfgang Kunz: “Gap-free Processor Verification by S2QED and Property Generation”, Design Automation and Test in Europe (DATE), 2020.
Summary: This paper describes a new formal technique for verifying the functional correctness of processors. Compared to the state of the art, this new approach requires only little manual effort (and costs).
Impact: This new approach has been adopted by Infineon and has become mainstream in Infineon's design flows for IoT platforms.
[9] Christian Bartsch, Stephan Wilhelm, Daniel Kästner, Dominik Stoffel and Wolfgang Kunz: Compositional Fault Propagation Analysis in Embedded Systems Using Abstract Interpretation, IEEE International Test Conference (ITC), October 2021.
Summary: This work provides the first complete formal framework to analyze the effect of HW faults at higher software levels. The approach scales to systems with hundreds of thousands of lines of software code. This results from leveraging Abstract Interpretation, a technique originating in Compiler technology and, so far, never having been applied in a context like this.
Impact: Similar as Paper [3], this basic research work proposes a radically new solution to an important problem by creating a new link between the traditional formalisms of the EDA field and another mathematical domain, such as Computer Algebra (Paper [3]) and Abstract Interpretation (this paper).
This research is a collaborative effort with the company AbsInt, https://www.absint.com/, (co-authors Wilhelm and Kästner). AbsInt is currently investing into this approach for safety analysis in automotive systems and avionics.
[10] J. Müller; Mo Fadiheh; A. Duque Anton; T. Eisenbarth; D. Stoffel and W. Kunz: “A Formal Approach to Confidentiality Verification in SoCs at the Register Transfer Level“, 58th IEEE/ACM Design Automation Conf. (DAC’21), Dec. 2021.
Summary: This is a major extension of the security analysis of Paper [6] to cover not only side channels but also security-critical design bugs. This promises a unified verification approach to security analysis for hardware fully covering the most relevant vulnerabilities at the microarchitectural level.
Impact: The method has detected severe security bugs in a previously well verified commercial processor. It has had impact also on the development of several open-source RISC-V cores and platforms, for example by reporting a number of security-critical bugs in the RISC-V Pulpissimo platform. Like for [6], the technology is currently being transferred to OneSpin (Siemens EDA). Only few weeks ago, Intel, Corp. USA, has declared its support also to this work by integrating Prof. Kunz and his team into Intel’s internal “Scalable Assurance” program (also providing further funding to this research).
