Day 3 - Thursday, 20 Nov 2014



09:00 - 09:50 Keynote: Navigating The Perfect Storm: New Trends in Functional Verification,
Harry Foster, Mentor Graphics
Session Chair: Ronny Morad

Abstract: Between 2006 and 2014, the average number of IPs integrated into an advanced SoC increased from about 30 to over 120. In the same period, the average number of embedded processors found in an advanced SoC increased from one to as many as 20. However, increased design size is only one dimension of the growing verification complexity challenge. Beyond this growing functionally phenomenon are new layers of requirements that must be verified. Many of these verification requirements did not exist ten years ago, such as multiple asynchronous clock domains, interacting power domains, security domains, and complex HW/SW dependencies. Add all these challenges together, and you have the perfect storm brewing. This talk introduces today's trends and challenges in SoC design and then discusses emerging verification strategy to navigate the perfect storm.

Bio: Harry Foster is Chief Scientist for Mentor Graphics' Design Verification Technology Division. He holds multiple patents in verification and has co-authored six books on verification. Harry was the 2006 recipient of the Accellera Technical Excellence Award for his contributions to developing industry standards, and was the original creator of the Accellera Open Verification Library (OVL) standard.

09:50 - 10:20 Break

10:20 - 11:50 Industry Special Session
Chair: Eli Arbel
This special session will host industry experts who will share their hands-on experience in hardware design and verification. We will have a unique opportunity to investigate real-life practices and solutions used in various companies in order to successfully develop and verify their chip designs. The session will cover topics related to validation of firmware-hardware flows in SoC, using emulation in SoC projects, and applying software paradigms in the hardware verification domain. This session is intended both for people from the industry, who will hear about other companies' challenges and solutions, as well as for academics, who can gain insight into what the industry is struggling with.

Validation of SoC Firmware-Hardware Flows: Challenges and Solution Directions,
Eli Singerman, Intel

Benefits of IP Level Emulation in an SoC Project,
Yaniv Dahan, Qualcomm

Applying Test-Driven Development Methods to Design Verification Software,
Efrat Shneydor, Cadence

11:50 - 12:20 Break

12:20 - 13:05 Tool Session
Chair: Alexander Ivrii

DynaMate: Dynamically Inferring Loop Invariants for Automatic Full Functional Verification,
Juan Pablo Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, and Andreas Zeller

Suraq - A Controller Synthesis Tool using Uninterpreted Functions,
Georg Hofferek and Ashutosh Gupta

Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study,
Mikhail Lukin, Maxim Buzdalov, and Anatoly Shalyto

13:05 - 14:05 Lunch

14:05 - 14:50 HVC Award Session
Chair: Eran Yahav

Synthesizing Software Verifiers from Proof Rules,
Andrey Rybalchenko, Corneliu Popeea, Nuno Lopes, and Sergey Grebenshchiko

Bio: Andrey Rybalchenko is a senior reseacher in the Programming Principles and Tools group at Microsoft Research. His research focuses on automated methods and tools for formal software verification and synthesis. In the past, Andrey was a professor at Technische Universität München and a reseach group leader at Max Planck Institute for Software Systems, a post-doc at EPFL, an intern at Microsoft Research Cambridge, a phd student at Max Planck Institute for Informatics, and a master's student at University of Saarland. Andrey received an ERC Starting grant (2012) and Microsoft Research European Fellowship (2006), was selected for MIT TR35 (2010) and Otto Hahn Medal (2005).

14:50 - 15:20 Break

15:20 - 16:40 Technical Session: Concurrency and Relaxed Models
Chair: Sharon Keidar-Barner

Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures,
John Derrick, Graeme Smith, Brijesh Dongol, and Lindsay Groves

Handling TSO in Mechanized Linearizability Proofs,
Oleg Travkin and Heike Wehrheim

A Framework to Synergize Partial Order Reduction with State Interpolation,
Duc-Hiep Chu and Joxan Jaffar

Partial Order Reduction for Multi-Core LTL Model Checking,
Alfons Laarman and Anton Wijs

16:40 - 16:55 Closing Remarks

play video


Keynote Speakers

  • Prof. Moshe Vardi, Rice University
  • Wolfgang Roesner, Fellow, IBM
  • Prof. Martin Vechev, ETH Zürich
  • Harry Foster, Chief Verification Scientist, Mentor Graphics
  • Ziv Binyamini, Corporate VP & CTO, System and Software Solutions, Cadence

Previous Conferences

%%sidebarspace%%
See us on Linked In See us on Facebook IBM Research Cadence Mellanox JASPER Qualcomm Mentor Graphics