Electrical & Computer Engineering     |     Carnegie Mellon

Tuesday, February 19, 12:15-1:15 p.m. HH-1112


Valeria Bertacco
Carnegie Mellon University

Towards Correctness-Constrained Execution for Processor Designs

Every integrated circuit is released with latent bugs. The damage and risk implied by an escaped bug ranges from almost imperceptible to potential tragedy; unfortunately it is impossible to discern within this range before a bug has been exposed and analyzed. While the past few decades have witnessed significant efforts to improve verification methodology for hardware systems, these efforts have been far outstripped by the massive complexity of modern digital designs, leading to product releases for which an always smaller fraction of system's states has been verified. The news of escaped bugs in large market designs and/or safety critical domains is alarming because of safety and cost implications (due to replacements, lawsuits, etc.).

This talk will describe our solutions to solve the verification challenge, such that users of future designs can be assured that their devices can operate completely free of bugs. We will attack the problem both at design-time, by presenting techniques to boost the fraction of the state space that can be verified before tape-out, and after deployment in the field, discussing novel solutions which can correct escaped bugs after a system has been shipped. Our ultimate vision for this technology is to make hardware as malleable as software.


Valeria Bertacco is an Assistant Professor of Electrical Engineering and Computer Science at the University of Michigan. Her research interests are in the areas of formal and semi-formal design verification, with emphasis on full design validation, and digital system reliability. Valeria joined the faculty at Michigan after being in the Advanced Technology Group of Synopsys for four years as a lead developer of Vera and Magellan, two popular verification tools. In 2005, she authored a book on symbolic simulation. Valeria serves in several conference program committees, including DATE, DAC and ICCAD, and she is an Associated Editor for the IEEE Transactions on CAD. In addition, she has been leading the effort for the development of the verification section in the International Technology Roadmap for Semiconductors report since 2004. She received her M.S. and a Ph.D. degree in Electrical Engineering from Stanford University in 1998 and 2003, respectively.