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

Dr. Andreas Keulmann

Cadence Berkeley Labs

The Application of Formal Methods
in Equivalence Checking & Property Verification

Abstract:

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.