Newsroom > Web Articles

 

Hardware/Software Codesign of Embedded Systems, Design Modeling and Design Verification

July 29, 2004 -- In late June, researchers from Calit² and the Jacobs School of Engineering participated in the Second ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), which took place in San Diego. UCSD computer science and engineering professor Rajesh Gupta, founding chair of the forum, served on its six-member Steering Committee, and Calit² researcher Ingolf Krueger chaired the committee on local arrangements. Krueger is also an assistant professor in residence within the Jacobs School's Computer Science and Engineering department.

UCSD computer science professor Rajesh Gupta (left) and Calit² researcher Ingolf Krueger helped organize the 2004 conference.

The long-term goal of MEMOCODE, outlined at its first annual conference in France in 2003, is to bring together theory and practice for embedded systems design, design modeling and design verification. "The overarching goal of this research community is to find ways to handle the ever-increasing complexity (defined by the size and diversity of function) of microelectronic systems-on-chip," explains Gupta, who holds the QUALCOMM Endowed Chair in Embedded Microsystems. "But it is proving difficult to improve the design and verification of these complex chips, at least at the pace set by process technology based on Moore's Law and the complexity of the embedded software. This has created a design productivity gap. We have now arrived at a situation where our ability to correctly design, validate microelectronic systems-on-chip, or to use these in exciting new applications from automotive to sensor-based systems is significantly behind the semiconductor manufacturing capabilities. So the new chips come out of the fabrication in large volumes in a very short time, much shorter than typical product trial and testing cycles. This is leading to nightmare scenarios of missed market windows, product opportunities and massive scale product recalls. There is no question that going forward, design technology will be a limiter on progress of microelectronic system capabilities."

This year's conference covered a wide range of related topics, including formal specification languages, formal models, model checking, theorem proving, specification-based testing, compositional methods, methodologies based on formal methods, and rigorous approaches (e.g., refinement) to transforming a hardware or software specification into a reliable, efficient implementation. Keynote speakers for the 2004 event included Randy Bryant of Carnegie-Mellon University; UC Berkeley's Edward A. Lee; and David Dill of Stanford University.

One underlying theme was the convergence of formal methods and industrial trends. To underscore the topic, "we brought together a panel of industry experts to talk about the future of software verification, given that hardware verification has been such an uphill battle," explains MEMOCODE co-chair Sandeep Shukla, of Virginia Tech. The panel was chaired by Tevfik Bultan of UC Santa Barbara, and participants included research officials from Mentor Graphics, Cadence, Microsoft, Intel, Synopsis and NASA's Jet Propulsion Laboratory. Streaming video of each industry presentation is now available for on-demand viewing, along with a panel discussion moderated by Virginia Tech's Shukla [RealOne or RealPlayer required]:

VIDEOS Brian Bailey, Mentor Graphics "Is formal being squeezing out functional verification" [Video] Gerard Holzman, Jet Propulsion Laboratory "Formal methods and software" [Video] Bob Kurshan, Cadence "Formal Verification As a Technology Transfer Problem" Length: 19:57 [Video] Vladimir Levin, Microsoft "Static Driver Verifier, a formal verification tool aimed at Windows device drivers" Length: 15:54 [Video]

VIDEOS John O'Leary, Intel "Formal Verification in Intel CPU Design" Length: 19:00 [Video] Carl Pixley, Synopsis "Designers Want Proofs! But Show Me the Money" Length: 19:53 [Video] Sandeep Shukla, Virginia Tech, et. al. "Panel Discussion" [Video]

"This year's meeting underscored how pervasive systems on chip and related systems are becoming, as well as the need for bringing together software and hardware domain experts," says Calit²'s Krueger. "This is of vital interest to Calit² because embedded systems including sensors are increasingly networked and highly interrelated."

MEMOCODE 2004 was supported by the Office of Naval Research, the National Science Foundation, BlueSpec Incorporated, INRIA-IRISA, and the UC Discovery Grant program. (Streaming video hosted by Calit².)