EECS Joint Colloquium Distinguished Lecture Series

Wednesday, November 28, 2001
Hewlett Packard Auditorium, 306 Soda Hall
4:00-5:00 p.m.

Dr. Andreas Keulmann

Cadence Berkeley Labs

Print Version

The Application of Formal Methods
in Equivalence Checking & Property Verification




In this presentation we will discuss the application of formal methods in hardware verification. The first part of the talk covers the area of functional equivalence checking. After an introduction into the problem, we will demonstrate how a fine-tuned combination of a contemporary design methodology with a set of specialized algorithms can reduce the practical complexity of equivalence checking and provide a robust solution for a wide range of applications. In the second part of the talk we will discuss recent research results in the area of reachability analysis, a core algorithm needed for formal property verification. We will show that similar to its success in logic synthesis and equivalence checking, a gradual, transformation-based approach can exploit problem-specific structures and thus offer a promising direction to significantly boost the capacity of current algorithms.


Andreas Kuehlmann received the Dipl-Ing. degree and the Dr.-Ing. habil degree in Electrical Engineering from the University of Technology at Ilmenau, Germany, in 1986 and 1990, respectively. His research topics included algorithms for automatic layout verification and synthesis.

From 1990 to 1991, Dr. Kuehlmann worked at the Fraunhofer Institute of Microelectronic Circuits and Systems Duisburg on a project to automatically synthesize embedded microcontrollers. As part of that work, he participated in the design of a dashboard controller for automotive applications. In 1991, Andreas Kuehlmann joined the IBM T.J. Watson Research Center where he worked until June 2000 on various projects in high-level and logic synthesis and hardware verification. Among others, he was the principal author and project leader of the Verity tool, IBMs standard equivalence checker, which is used company-wide to verify microprocessor and ASIC designs. From January 1998 until May 1999 he visited the Department of Electrical Engineering and Computer Science at UC Berkeley. In July 2000 he joined the Cadence Berkeley Labs where he continues to work on synthesis and verification problems.