Data e Ora: 
Thursday, March 2, 2006 - 15:00
Luogo: 
Aula Magna `Antonio Lepschy`
Relatore: 
Valeria Bertacco
Descrizione: 

The verification of modern computing systems has grown to dominate the cost of system design, often with limited success, as designs continue to be released with latent bugs. This trend is accelerated with the advent of highly integrated system-on-a-chip (SoC) designs, which feature multiple complexᅠ subcomponents connected by simultaneously active interfaces. To cope with this challenge, logic simulation techniques are predominant in the industry, however, the coverage of the tests generated is usually low, with the result that even months of simulation provide little confidence in the correctness of
the design and, when design errors are found, the error analysis phase is daunted by long and complex bug traces. Additionally, these traditional techniques require a lot of effort from the engineering team to direct the verification activity towards specific design areas of critical quality. Nonetheless, they have such high inertia in existing development processes that the cost to transition to alternative methodologies, such as formal techniques, is high.
In this talk, I will introduce a new generation of hybrid verification solutions, which we call LOW MAINTENANCE VERIFICATION, where the contribution of formal techniques is transparently deployed within a simulation-based verification framework. Our use of formal techniques in this context greatly enhances the level of automation of the verification process, by generating solutions that can focus on a verification goal with minimal guidance from the engineer. I will overview some of the solutions that we developed in this space: Guido and StressTest, two solutions that can automatically generate `interesting` verification scenarios. Our preliminary experience in the domain of low maintenance verification indicates that this family of techniques can effectively lead to high-performance, high-coverage verification solutions, by generating concise error traces with minimal demands on verification engineers and no change in the verification process.
Finally, I will briefly provide some highlights from recent architecture and CAD research at the EECS department of the University of Michigan.

Affiliazione: 
University of Michigan, USA