Robert Kurshan Fellow, Cadence Design Systems
From EMC to EDA
CMU's EMC (Existential Model Checker) started a long but straight path to EDA (Electronic Design Automation), the industry concerned with testing commercial circuit designs. I'll describe where the industry is today and explain how that path got us here.
Robert Kurshan joined Cadence Design Systems in 2001. Before that, he was a Distinguished Member of Technical Staff at Bell Laboratories, Murray Hill, NJ, until his retirement in 2001. He worked at Bell Labs since receiving his Ph.D in mathematics in 1968, from the University of Washington under James Jans, in homological algebra. Under special arrangement with Bell Labs, he spent two years as Visiting Professor at the Technion (Haifa, Israel) in the departments of Mathematics (1975-76) and Electrical Engineering (1984-85). In addition, he has taught courses at U.C. Berkeley and N.Y.U. At Bell Labs, he did research in periodic sequences, digital filtering and approximation theory, before he began work in formal verification in 1983. He is an author of over 80 technical publications, holds 22 patents in communications, digital filtering and verification, and is the author of the book Computer-Aided Verification of Coordinating Processes (Princeton Univ. Press, 1994) which is based upon courses he gave at U. C. Berkeley and the Technion.
In connection with his work in verification, he designed and built the COSPAN verification system together with Zvi Har'El, Ronald H. Hardin, and a number of others, based upon the theory that is developed in his book. COSPAN has been in use (and continuous development) since 1986, having been applied directly to a number of commercial projects inside AT&T, Lucent, NCR and Intel, as well as having been licensed to numerous universities for educational use. Currently, COSPAN is marketed by Cadence Design Systems for commercial hardware verification, under the trademark FormalCheck. In 1998, FormalCheck won the Innovation of the Year Award, from EDN. More recently, SAT-based algorithms from Cadence Berkeley Labs have been integrated into COSPAN, which has been released in a new simplified tool for fully automated assertion-based verification called ISV. Other related applications include constraint solving and automatic test bench generation.