Home	Conference Program	Advisory Board	Exhibition	Registration	Practical Information

Seminar: A Formal Approach to Low Power Verification

In recent years, there are two dominant areas in technologies cause by making electronic devices more mobile and versatile. First area is in SOC (System-on-chip) areas utilizing smaller IPs as building-blocks to allow flexibilities in customizing features and faster time-to-market. Second area is in low-power design where more and more capable hardware is introduced into an SOC that requires good power-consumption. Consequently, many SOC designs have applied aggressive low-power features such as power-domains to reduce the power-consumption in SOC level. Besides the challenges of power-architecture, power estimation and power-reductions, the addition of power-domains has increased the complexity of verification by a large factor.

In this presentation, we will present some of the challenges faced in subsystems low-power verification, and how Jasper’s Low-power Formal solution is being leveraged to tackle various verification challenges. In terms of verification challenges, it starts from the fact that the design behavior is now a combination of RTL and power-specification (UPF, CPF etc.) which introduce many new corner cases that affect normal functionalities. Next, there are also changes needed to be done on a typical SOC to incorporate power-controls and interaction with each unit within the subsystem to ensure proper low-power behaviors. Finally, there are integration challenges as power-domains are typically defined after integration of IPs into a subsystem.

The solutions include three main areas: First is the exploration of power-sequences to the different power-domains as well as verification of normal functionalities after the insertion of power-domains and controls. Second is to enabling power-aware formal verification to verify low-power behavior and confirm differences (or lack of) before and after power-domain insertion. Finally, with the power-aware model, we will verify various integration aspects of SOC.

Speakers:

		Barbara Jobstmann Senior Field Applications Engineer Jasper Design Automation
	Barbara Jobstmann is a Senior Field Applications Engineer for Jasper Design Automation. She also holds a researcher position at the French National Research Center (CNRS). Prior to Jasper, Barbara was working in academic research labs in France and Switzerland focusing on constructing correct and reliable systems using formal verification and synthesis techniques. Barbara holds a PhD in Computer Science from Graz University of Technology, Austria.
		Frédéric Rocheteau R&D manager STMicrolectronics
	Frédéric Rocheteau has 20 years of experience in the semiconductor and EDA industries on circuit design tools and methodologies development, with a particular focus on formal verification techniques. He is currently R&D manager at STMicrolectronics, in charge of providing advanced tools and flows to IPs and libraries design teams. Frédéric Rocheteau holds a Ph.D. in Computer sciences from the Institut National Polytechnique de Grenoble (INPG)