Andreas Kuehlmann
Biography
From 1990 to 1991, he worked at the Fraunhofer Institute of Microelectronic Circuits and Systems, Duisburg, on a project to automatically synthesize embedded microcontrollers. In 1991 he 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 Verity, IBM's standard equivalence checking tool. From January 1998 until May 1999, Andreas visited the Department of Electrical Engineering and Computer Science at U.C. Berkeley. In July 2000, he joined the Cadence Berkeley Laboratories where he continues to work on synthesis and verification problems. Since July 2002, he is also adjunct professor at the University of California at Berkeley. In 2003, Andreas was awarded IEEE Fellow. In August 2003, Andreas became the Director of Cadence Laboratories and was also promoted to Cadence Fellow in 2004.
Selected Publications
- Q. Zhu, N. Kitchen, A. Kuehlmann, and A. L. Sangiovanni-Vincentelli, "SAT sweeping with local observability don't-cares," in Proc. 43rd ACM/IEEE Design Automation Conf. (DAC 2006), New York, NY: The Association for Computing Machinery, Inc., 2006, pp. 229-234.
- D. Chai and A. Kuehlmann, "A fast pseudo-Boolean constraint solver," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 24, no. 3, pp. 305-317, March 2005.
- A. Kuehlmann, "Dynamic transition relation simplification for bounded property checking," in Proc. IEEE/ACM Intl. Conf. on Computer-Aided Design, Piscataway, NJ: IEEE Press, 2004, pp. 50-57.
- A. Kuehlmann, V. Paruthi, F. Krohm, and M. K. Ganai, "Robust Boolean reasoning for equivalence checking and functional property verification," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 21, no. 12, pp. 1377-1394, Dec. 2002.
- A. Kuehlmann and J. Baumgartner, "Transformation-based verification using generalized retiming," in Lecture Notes in Computer Science: Computer Aided Verification, G. Berry, H. Comon, and A. Finkel, Eds., 2102 ed., London, UK: Springer-Verlag, 2001, pp. 104-117.
- A. Kuehlmann and F. Krohm, "Equivalence checking using cuts and heaps," in Proc. 34th Design Automation Conf., New York, NY: ACM Press, 1997, pp. 263-268.
- D. P. Appenzeller and A. Kuehlmann, "Formal verification of a PowerPC microprocessor," in Proc. 1995 IEEE Intl. Conf. on Computer Design: VLSI in Computer and Processors, Los Alamitos, CA: IEEE Computer Society Press, 1995, pp. 79-84.
- A. Kuehlmann, A. Srinivasan, and D. P. LaPotin, "Verity - A formal verification program for custom CMOS circuits," IBM J. Research and Development, vol. 39, no. 1-2, pp. 149-165, Jan. 1995.
- A. Kuehlmann, D. I. Cheng, A. Srinivasan, and D. P. LaPotin, "Error diagnosis for transistor-level verification," in Proc. 31st ACM/IEE Conf. on Design Automation, New York, NY: ACM Press, 1994, pp. 218-224.
Photo
