Computer Engineering Seminar

Assertion Mining: What, How and Where?

Graziano Pravadelli

Associate Professor
University of Verona (Italy)
Wednesday, October 05, 2016
1:00pm - 2:00pm
3725 Beyster

Add to Google Calendar

About the Event

Since the last decade, assertion-based verification (ABV) has emerged as one of the most promising solutions for system-level verification. ABV relies on the definition of logic formulas (assertions) that formalize the behaviours of the design under verification (DUV) by overcoming the ambiguity of natural languages and providing the engineers with precise and well-defined specifications. However, the definition of assertions is a time-consuming process that requires high expertise and sometime terminates with an incomplete, but redundant, set of assertions. This makes the ABV process precarious and uselessly long. To overcome the limitations of a manual definition, this talk will deal with assertion mining as a complementary approach for the automatic generation of assertions. After the introduction of the key concepts, the talk will present a way for dynamically extracting assertions from the simulation traces of the DUV. Then, it will show how mined assertions can be used to automatically generate the basic blocks of a system level virtual prototype for the verification of both functional and extra functional properties of the DUV. In particular, two methodologies will be described that use assertion mining to generate, respectively, functional test patterns and power state machines.


Graziano Pravadelli, IEEE senior member, is an associate professor at the Computer Science Department of the University of Verona (Italy) and co-founder of EDALab s.r.l. (Italy). He received the Laurea Degree and the PhD in Computer Science at University of Verona, respectively in 2001 and 2004. In 2007, he co-founded EDALab s.r.l., an Italian SME whose mission consists of giving support for innovation and technology transfer in embedded system modeling and verification. His main interests focus on modeling, simulation and semi-formal verification of HW/SW embedded systems and cyber physical systems, with particular regards to virtual prototyping, correct-by-construction HW/SW manipulation, TLM and RTL modeling, abstraction and refinement techniques, mutation analysis and mutation testing, functional qualification and assertion-based verification. In this context, he collaborated in several national and European projects (e.g., VERTIGO, COCONUT, COMPLEX, SMAC, CONTREX) and he published more than 100 papers in international conferences and journals. He is involved in the committees of international conferences like DATE, CODES+ISSS, VLSI-SoC, and FDL.

Additional Information

Sponsor(s): CSE

Open to: Public