Dr. Kurshan will describe a new project in Cadence to develop a tool set that supports abstraction in the context of hierarchial design.
Abstract / Event Description:
Verification coverage does not scale gracefully with growing system design size. Component interactions grow exponentially with the number of system components, while conventional system test at best can increase coverage as a linear function of alloted test time.
Likewise, capacity limitations are commonly cited as the essential gating factor that restricts the application of automatic formal verification (model checking) to at most a few design blocks.
Nonetheless, abstraction has long been used successfully in pilot projects to apply model checking to entire systems. Abstraction in conjunction with guided-random simulation can be used in the same way to increase coverage for conventional test.
Dr. Kurshan will describe a new project in Cadence to develop a tool set that supports abstraction in the context of hierarchial design.
BIO:
Robert Kurshan joined Cadence Design Systems, Inc. as a Fellow, 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 in homological algebra.
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, "Computer-Aided Verification of Coordinating Processes" (Princeton Univ. Press, 1994).
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 utilized by Cadence for commercial hardware verification in its IFV product and for constraint-solving in its guided-random simulator product IUS.
In 2005 he was a joint recipient of the ACM Kanellakis Theory and Practice Award for his work in automata-theoretic verification.
