Keynote Speech II
16:40–17:40, Monday, October 24, 2022
One is not Enough: Using Hybrid Proof Engines for Polynomial Formal Verification
Rolf Drechsler
University of Bremen/DFKI
Abstract
Recently, polynomial formal verification has been introduced as a new concept. The core idea is to consider verification not only as a post-processing step, but from the very beginning. Based on formal proof techniques complexity bounds are given that allow for an efficient verification task. Thus, this overcomes the unpredictability problem and ensures the scalability of verification techniques. Despite this progress, most of the works are still limited to the polynomial verification of individual components, e.g. adders and multipliers, and are based on a monolithic proof engine. Polynomial formal verification of complex systems, consisting of many different sub-components, is an almost unexplored area. The challenge originates from the fact that a verification method (e.g., BDD-based equivalence checking) might verify a sub-component (e.g., an adder) in polynomial time but have an exponential verification complexity for another component (e.g., a multiplier).
The concept of polynomial verification is reviewed. Then, we introduce a hybrid verification engine to attack the problem of verifying complex modern systems in polynomial space and time. The engine takes advantage of several verification techniques, such as combinational equivalence checking based on bit-level approaches, like SAT and BDDs, as well as word-level verification based on e.g. SCA and *BMDs. The correctness of each block or system task can be ensured in polynomial time using a specific verification technique from the environment. Thus, we overcome the shortcomings of using only one verification method and pave the way toward polynomial verification of advanced CPUs, DSP blocks, and AI-synthesized architectures.
The full paper version of this keynote speech is available in the proceedings: Rolf Drechsler and Alireza Mahzoon, “One is not Enough: Using Hybrid Proof Engines for Polynomial Formal Verification,” in Proc. SASIMI 2022, Oct. 2022.
Biography
Rolf Drechsler received the Diploma and Dr. phil. nat. degrees in computer science from the Johann Wolfgang Goethe University in Frankfurt am Main, Germany, in 1992 and 1995, respectively. He worked at the Institute of Computer Science, Albert-Ludwigs University, Freiburg im Breisgau, Germany, from 1995 to 2000, and at the Corporate Technology Department, Siemens AG, Munich, Germany, from 2000 to 2001.
Since October 2001, Rolf Drechsler is a Full Professor and Head of the Group of Computer Architecture, Institute of Computer Science, at the University of Bremen, Germany. 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. He is an ACM Distinguished Member and an IEEE Fellow.