HLDVT’16 Program

Friday, October 7th, 2016

 

Registration: 7:30 a.m. – 5:00 p.m.                                                                                             

Continental Breakfast: 7:30 – 8:30 a.m .                                                                                  

8:15 – 8:30 a.m.: Welcome Address                                                            

8:30 – 9:30 a.m.: Keynote Talk

Designing Fast and Accurate Stochastic Circuits

John P. Hayes (University of Michigan, U.S.A.)                                                           

Stochastic computing (SC) is an unconventional computing technique that processes data represented by pseudo-random bit-streams denoting probabilities. It enables complicated arithmetic functions to be implemented by tiny, low-power logic circuits. It is well-suited to applications that need massive parallelism or operate in noisy environments where conventional binary designs are too costly or too unreliable. SC has come to be seen as an attractive choice for tasks such as biomedical image processing and decoding complex error-correcting codes. Despite its desirable properties, SC has features that limit its usefulness, including low accuracy and long run times. This talk reviews SC, with a focus on how the randomness of its bit-streams, or the lack thereof (correlation), affects accuracy and speed. We show that correlation-induced errors can be reduced by the careful insertion of delay elements. We also discuss a desirable property of SNs called progressive precision, whereby accuracy increases predictably with bit-stream length.                                                                             

Session 1: Assertions and Properties                                                                               

Session Chair: Masahiro Fujita (University of Tokyo, Japan)

9:30 – 9:55 a.m.: Synthesizable SVA Protocol Checker Generation Methodology Based on TDML and VCD File Formats

Authors:

Mohamed O. Kayed (Mentor Graphics, Egypt)

Mohamed Abd El Salam (Mentor Graphics, Egypt)

Rafik Guindi (Nile University, Egypt)                                                                                    

9:55 – 10:20 a.m.: Accelerating Assertion Assessment Using GPUs

Authors:

Jason G. Tong (McGill University, Canada)

Marc Boulé (Ecole de Technologie Superieure, Canada)

Zeljko Zilic (McGill University, Canada)                                                                                

10:20 – 10:45 a.m.: Control-Flow Guided Clause Generation for Property Directed Reachability

Authors:

Xian Li (University of Kaiserslautern, Germany)

Klaus Schneider (University of Kaiserslautern, Germany)           

10:45 – 11:00 a.m.: Coffee Break                                                                           

Session 2: Behavioral Modeling and Specification                                         

Session Chair: Priyank Kalla (University of Utah, U.S.A.)     

11:00 – 11:25 a.m.: Log2model: Inferring Behavioral Models from Log Data

Authors:

Kasper S. Luckow (Carnegie Mellon University Silicon Valley, U.S.A.)

Corina S. Pasareanu (NASA Ames Research Center, U.S.A.)

11:25 – 11:50 a.m.: Formal Semantics of Behavior Specifications in the Architecture Analysis and Design Language Standard

Authors:

Loic Besnard (INRIA & IRISA, France)

Thierry Gautier (INRIA & IRISA, France)

Clement Guy (INRIA & IRISA, France)

Paul Le Guernic (INRIA & IRISA, France)

Jean-Pierre Talpin (INRIA & IRISA, France)

Brian R. Larson (FDA, U.S.A.)

Etienne Borde (Telecom ParisTech, France)

11:50 – 12:15 p.m.: Specification by Existing Design Plus Use-Cases

Authors:

Yusuke Kimura (University of Tokyo, Japan)

Masahiro Fujita (University of Tokyo, Japan)                                                                      

12:15 – 1:15 p.m.: Lunch                                                  

Special Session 1: High-Level Modeling and Verification of Automotive/Transportation Systems                                              

Organizer: Sara Vinco (Politecnico di Torino, Italy)     

Session Chair: Grant Martin (Cadence, U.S.A.)                                                          

1:15 – 1:40 p.m.: Design Centric Modeling of Digital Hardware

Authors:

Johannes Schreiner (Infineon Technologies, Germany)

Rainer Findenig (Infineon Technologies, Austria)

Wolfgang Ecker (Infineon Technologies, Germany)

1:40 – 2:05 p.m.: Design Space Exploration for Deterministic Ethernet-Based Architecture of Automotive Systems

Authors:

Prachi Joshi (Virginia Tech, U.S.A.)

Vedahari Narasimhan Ganesan (Virginia Tech, U.S.A.)

Haibo Zeng (Virginia Tech, U.S.A.)

Sandeep K. Shukla (IIT Kanpur, India)

Chung-Wei Lin (Toyota InfoTech Center, U.S.A.)

Huafeng Yu (Boeing Research and Technology, U.S.A.)

2:05 – 2:30 p.m.: Fault Injection Ecosystem for Assisted Safety Validation of Automotive Systems

Authors:

Sebastian Reiter (FZI Forschungszentrum Informatik, Germany)

Alexander Viehl (FZI Forschungszentrum Informatik, Germany)

Oliver Bringmann (Universit¨at T¨ubingen, Germany)

Wolfgang Rosenstiel (Universit¨at T¨ubingen, Germany)

2:30 – 2:55 p.m.: Modeling, Programming and Performance Analysis of Automotive Environment Map Representations on Embedded GPUs

Authors:

Jörg Fickenscher (Friedrich-Alexander University Erlangen-N¨urnberg, Germany)

Oliver Reiche (Friedrich-Alexander University Erlangen-N¨urnberg, Germany)

Jens Schlumberger (Friedrich-Alexander University Erlangen-N¨urnberg, Germany)

Frank Hannig (Friedrich-Alexander University Erlangen-N¨urnberg, Germany)

Jürgen Teich (Friedrich-Alexander University Erlangen-N¨urnberg, Germany)                       

2:55 – 3:15 p.m.: Coffee Break                                                                                      

3:15 – 4:15 p.m.: Invited Talk

Harnessing Deep Analytics for the HW Verification Process

Avi Ziv (IBM, Israel)

Modern verification is a highly automated process in which an endless number of verification jobs are continuously being executed in verification farms. The process involves many tools and subsystems, handling tasks such as documentation and management of the verification plan, generate stimuli, simulate the design under verification, collect coverage data, and more.  These verification tools produce a large amount of data that is essential for understanding the state and progress of the verification process.  With the growing complexity and size of the verification process on the one hand and availability of more and more verification tools that produce a large amount of data on the other hand, we see a shift in the verification domain from a world that contains little data that forces verification engineers to walk in the dark to a world with too much data that can drown the verification team.

This talk discusses the challenges of converting the data produced by the verification process into insights into the state and progress of the process and actions that can improve them. The main weapon for tackling these challenges is deep analytics (statistical analysis, Machine Learning, etc.). It is shown how the analysis of the correlation of data from several sources can provide deep, otherwise hidden, insight into the verification state, thus enabling significant optimization.                

4:15 – 5:30 p.m.: Panel      

Killer Apps: Not Your Father’s Formal Verification 

There has been much talk recently about the increasing usage of easy to use formal verification tools that target light weight properties. Is this the future of formal verification or does it continue to lie in experts searching for hard to find bugs? Recently verification tools that are targeted at particular, relatively narrow, applications such as CDC, timing constraints, X pessimism/optimism, register checking etc. have begun to cross over into main-stream usage. Some of these applications combine structural, functional and formal analysis techniques. Are there “Killer apps” that will be the way forward to “crossing the chasm” for formal verification usage or is this just marketing hype, or something in-between?

Organizers: Eli Arbel (IBM, Israel), and Prab Varma (Real Intent, U.S.A.)

Moderator: Jim Hogan (Angels by the Sea, U.S.A.)

Panelists:

Raik Brinkmann (OneSpin Solutions, Germany)

Pete Hardee (Cadence, U.S.A.)

Viresh Paruthi (IBM, U.S.A.)

Erik Seligman (Intel, U.S.A.)  

Vigyan Singhal (Oski, U.S.A.)  

Syed Suhaib (NVIDIA, U.S.A.)                                                                             

5:30 – 6:30 p.m.: Beer and Wine Reception        

Saturday, October 8th, 2016

 

Registration: 7:30 a.m. – 5:00 p.m.                                                                                             

Continental Breakfast: 7:30 – 8:30 a.m .                                                                      

8:30 – 9:30 a.m.: Keynote Talk

Cross-Layer Resilience: Are High-Level Techniques Always Better?  

Jacob Abraham (University of Texas at Austin, U.S.A.)

Computers are pervasive in society because advances in semiconductor technology have enabled increased performance and reduced costs. In many critical applications, the computers need to continue operating correctly in spite of manufacturing defects as well as failures during operation due to wear-out or external disturbances. Resilience techniques across different layers of the system have been proposed for achieving the desired degree of resilience at minimal cost. This talk will discuss a comprehensive framework which enables the systematic analysis of resilience techniques across various layers of the system stack, and the surprising results obtained. Areas where high-level, application-level checks are appropriate will also be described.                               

Special Session 2: Medical Devices and Assisted Living: High-Level Design and Verification Approaches                                                                        

Organizers: Samarjit Chakraborty (Technical University of Munich, Germany), and Graziano Pravadelli (University of Verona, Italy)

Session Chair: Qi Zhu (University of California, Riverside, U.S.A.)                                    

9:30 – 9:55 a.m.: Dynamic Service Synthesis and Switching for Medical IoT and Ambient Assisted Living

Authors:

Daniel Yunge (Technical University of Munich, Germany)

Sangyoung Park (Technical University of Munich, Germany)

Philipp Kindt (Technical University of Munich, Germany)

Graziano Pravadelli (University of Verona, Italy)

Samarjit Chakraborty (Technical University of Munich, Germany)

9:55 – 10:20 a.m.: High-Level Modeling for Computer-Aided Clinical Trials of Medical Devices

Authors:

Houssam Abbas (University of Pennsylvania, U.S.A.)

Zhihao Jiang (University of Pennsylvania, U.S.A.)

Kuk Jin Jang (University of Pennsylvania, U.S.A.)

Marco Beccani (University of Pennsylvania, U.S.A.)

Jackson Liang (Hospital of the University of Pennsylvania, U.S.A.)

Rahul Mangharam (University of Pennsylvania, U.S.A.)

10:20 – 10:45 a.m.: Brain-Computer Interface using P300: A Gaming Approach for Neurocognitive Impairment Diagnosis

Authors:

Daniela De Venuto (Politecnico di Bari, Italy)

Valerio Francesco Annese (Politecnico di Bari, Italy)

Giovanni Mezzina (Politecnico di Bari, Italy)

Michele Ruta (Politecnico di Bari, Italy)

Eugenio Di Sciascio (Politecnico di Bari, Italy)                   

10:45 – 11:00 a.m.: Coffee Break                                                                 

Session 3: System Level Design & Simulation                                                  

Session Chair: John Barry (Intel, Ireland)         

11:00 – 11:25 p.m.: A Segment-Aware Multi-Core Scheduler for SystemC PDES

Authors:

Guantao Liu (University of California, Irvine, U.S.A.)

Tim Schmidt (University of California, Irvine, U.S.A.)

Rainer Doemer (University of California, Irvine, U.S.A.)

11:25 – 11:50 p.m.: Automatically Adjusting System Level Designs after RTL/Gate-Level ECO

Authors:

Qinhao Wang (University of Tokyo, Japan)

Yusuke Kimura (University of Tokyo, Japan)

Masahiro Fujita (University of Tokyo, Japan)

11:50 – 12:15 p.m.: A Unifying Flow to Ease Smart Systems Integration

Authors:

Michele Lora (University of Verona, Italy)

Sara Vinco (Politecnico di Torino, Italy)

Franco Fummi (University of Verona, Italy)                                                                         

12:15 – 1:15 p.m.: Lunch                                                                               

Session 4: Advances in Formal Verification and Test Generation

Session Chair: Sara Vinco (Politecnico di Torino, Italy)

1:15 – 1:40 p.m.: Estimation of Formal Verification Cost Using Regression Machine Learning

Authors:

Eman El Mandouh (Mentor Graphics Corporation, Egypt)

Amr G. Wassal (Cairo University, Egypt)                                          

1:40 – 2:05 p.m.: Hardware-in-the-Loop Model-Less Diagnostic Test Generation

Authors:

Sarmad Tanwir (Virginia Tech, U.S.A.)

Michael S. Hsiao (Virginia Tech, U.S.A.)

Loganathan Lingappan (Intel, U.S.A.)                                  

2:05 – 2:30 p.m.: Clock Domain Crossing Formal Verification: A Meta Model

Authors:

Mejid Kebaili (STMicroelectronics and Univ. Grenoble Alpes and CNRS, France)

Jean-Christophe Brignone (STMicroelectronics, France)

Katell Morin-Allory (Univ. Grenoble Alpes and CNRS, France)

2:30 – 2:55 p.m.: Word-Level Traversal of Finite State Machines Using Algebraic Geometry

Authors:

Xiaojun Sun (University of Utah, U.S.A.)

Priyank Kalla (University of Utah, U.S.A.)

Florian Enescu (Georgia State University, Atlanta, U.S.A.)                                              

2:55 – 3:15 p.m.: Coffee Break                                                                                       

Special Session 3: High-Level Modeling and Verification of Biological Systems                                                                                                

Organizer: Natasa Miskov-Zivanov (University of Pittsburgh, U.S.A.)         

Session Chair: Graziano Pravadelli (University of Verona, Italy)     

3:15 – 3:40 p.m.: Deciphering Cancer Biology Using Boolean Methods

Authors:

Subarna Sinha (Stanford University, U.S.A.)

David Dill (Stanford University, U.S.A.)

3:40 – 4:05 p.m.: SyQUAL: A Platform for Qualitative Modelling and Simulation of Biological Systems

Authors:

Rosario Distefano (University of Verona, Italy)

Nickolas Goncharenko (University of Toronto, Canada)

Franco Fummi (University of Verona, Italy)

Rosalba Giugno (University of Verona, Italy)

Gary Bader (University of Toronto, Canada)

Nicola Bombieri (University of Verona, Italy)           

4:05 – 4:30 p.m.: High-Level Modeling and Verification of Cellular Signaling

Authors:

Natasa Miskov-Zivanov (University of Pittsburgh, U.S.A.)

Paolo Zuliani (Newcastle University, U.K.)

Qinsi Wang (Carnegie Mellon University, U.S.A.)

Edmund M. Clarke (Carnegie Mellon University, U.S.A.)

James R. Faeder (University of Pittsburgh, U.S.A.)            

4:30 – 4:55 p.m.: Probabilistic Reachability Analysis of the Tap Withdrawal Circuit in Caenorhabditis elegans

Authors:

Md. Ariful Islam (Carnegie Mellon University, U.S.A.)  

Qinsi Wang (Carnegie Mellon University, U.S.A.)

Ramin M. Hasani (Vienna University of Technology, Austria)

Ondrej Balun (Vienna University of Technology, Austria)

Edmund M. Clarke (Carnegie Mellon University, U.S.A.)

Radu Grosu (Vienna University of Technology, Austria)

Scott A. Smolka (Stony Brook University, U.S.A.)

4:55 – 5:20 p.m.: Formal Modeling of Biological Systems

Authors:

Qinsi Wang (Carnegie Mellon University, U.S.A.)

Edmund M. Clarke (Carnegie Mellon University, U.S.A.)                                                                                                                                      

                                               

 

 

                                                                       

Tutorials

Friday, October 7th, 2016

9:30 a.m. – 10:45 a.m.: Tutorial 1

Word-Level Abstractions for Datapath Designs Using Algebraic Geometry

Priyank Kalla (University of Utah, U.S.A.)

Algebraic geometry is the study of the geometry of solutions to a system of polynomial equations. Modern algebraic geometry does not explicitly solve the system of equations to enumerate the solutions, but rather reasons about the solutions using abstract/computational algebra. It uses the tools and techniques of Groebner bases to solve such algebraic reasoning problems. Such techniques are very powerful—actually known to be strictly stronger than resolution based SAT—and they can be applied for design abstraction and verification both at the bit- and word-level using a unified framework. In this talk, I will describe how techniques from algebraic geometry and symbolic computation can be used to derive word-level abstractions of the functions implemented by datapath designs, and how such techniques can be applied to formal verification and also simulation-based verification.

Hardware designs and the underlying functions often exhibit some structure or symmetry in the implementations. To improve our understanding of such designs, the functionality, symmetry and the structure of the circuits has to be analyzed altogether. I will show that algebraic geometry with Groebner bases can be a very capable tool in that regard. Hopefully, this will motivate the HLDVT community to investigate these topics for high-level design abstraction and verification.

11:00 a.m. – 12:15 p.m.: Tutorial 2

Employing Trace Generation-Based Debugging Strategies for Modern Hardware and Software Development

Bojan Mihajlovic (Synopsys, U.S.A.)

In the era of non-deterministic hardware operation and software execution, the number of complex faults encountered during development is growing alongside the time and effort needed to resolve them. The situation has been exacerbated by the inability of traditional debugging strategies to adapt to such faults. Instead, the collection, recording, and analysis of trace data is presently recognized as the only means by which complex faults can be deterministically observed.

This talk will show how trace generation methodologies are applied alongside conventional debugging infrastructure, such as traditional execution-control methods and deterministic replay mechanisms. The on-chip hardware infrastructure that enables trace generation will be described, including hardware triggers and trace storage mechanisms. Typical software interfaces for exercising trace experiment control will also be described, as well as methods for extracting the resultant debugging data.

The advantages of using such debugging methods at different points in a development cycle will be discussed, including with simulated, emulated, and real hardware designs. Of particular interest in the verification domain will be the presentation of hardware infrastructure enabling unobtrusive observation of timing-based faults. A typical debugging session will be depicted which involves the observation of a complex fault using a combination of conventional and trace-based debugging.

The discussion will also explore ongoing implementation and research challenges, including unobtrusive operation, granularity of observation, trace data volume, as well as the qualification and interpretation of what constitutes relevant trace data. Recently-proposed solutions to selected problems will be presented, including techniques for hardware compression of common trace data types.          

1:15 p.m. – 2:30 p.m.: Tutorial 3

Combining Formal Proof and Testing

Kenneth McMillan (Microsoft, U.S.A.)

While full formal proof of complex systems remains a challenge, formal methods can readily be applied in practice to improve the performance of testing in exposing design errors. A good example of this is compositional testing. In this methodology each component of a system is given a formal specification and it is proved formally that these specifications guarantee system-level correctness. The components are then rigorously tested against their formal specifications. This approach has the advantages of unit testing in covering component behaviors, while at the same time exposing all system-level errors to testing. Moreover, it can expose latent bugs in components that are not stimulated in the given system but may occur when the component is re-used in a different environment. This tutorial will cover the basics of compositional testing by example, introducing the available tools, and will also discuss industrial applications.