Osmosis 2020 | December 1–2 | Virtual Event
What is Osmosis?
Osmosis stands for OneSpin Meeting on Solutions, Innovation, & Strategy. It is a users’ group for customers and partners of OneSpin Solutions, provider of electronic design automation (EDA) tools for integrated circuit (IC) integrity verification. Osmosis signifies balance and two-way movement—in this case, of technical knowledge and expertise among OneSpin's experts and users.
This users' group meeting is tailored for current and users of OneSpin 360™ verification solutions, but we welcome prospective users on a case-by-case basis. If IC integrity is important to you—particularly in the areas of functional correctness, safety, security, or trust—then this event is for you!
Due to the COVID-19 pandemic, this year's Osmosis will be a virtual event held over two consecutive afternoons. Last year, we gathered in Munich for a hard-hitting technical agenda and capped off the day with a festive Bavarian dinner. We will dearly miss seeing all of you in person, but we look forward to this opportunity to reconnect and to learn from fellow IC integrity enthusiasts!
Day 1 At-A-Glance
Tuesday, December 1, 2020 | 13:00 CET (UTC +1)
Keynote Address: Raik Brinkmann, President & CEO, OneSpin
User Case Studies:
OneSpin Technical Deep Dives:
- Functional Correctness
- FMEDA Automation & Safety
- Trust & Security
Day 2 At-A-Glance
Wednesday, December 2, 2020 | 13:00 CET (UTC +1)
Keynote Address: Claudionor José Nunes Coelho, VP/Fellow of AI – Head of AI Labs, Palo Alto Networks
User Case Studies:
OneSpin Technical Deep Dives:
Breakout Sessions with OneSpin's Experts:
- The Ins and Outs of Trust & Assurance
- RISC-V and the Open Source Movement
- FMEDA and Verification: Which Side Are You On?
Read on for the complete agenda—including session times and abstracts—and additional details!
Full Agenda for Osmosis 2020
Click to expand each day's agenda detailsAll times are shown in Central European Time (CET / UTC +1) and are subject to change
13:00 Welcome to Osmosis, Day 1
OneSpin Master of CeremoniesAgenda overview and event logistics
13:05 Opening Keynote Address: IC Integrity in Today's Evolving World
Raik Brinkmann, President & CEO, OneSpinWhen we say "IC integrity," what do we mean? On the surface, we are addressing the functional correctness of a design, but there's much more to it than that: safety, security, and trust all come into play in myriad ways and can vary widely with the market vertical and end use of an ASIC, FPGA, or SoC. To open this year's Osmosis event, President and CEO Raik Brinkmann explores the far-reaching and nuanced ramifications of IC integrity—and the potentially dire consequences of a lack thereof—in today's increasingly connected, automated, electronically-dependent world. From this broader context, Raik will then draw back the curtain and offer Osmosis attendees privileged insights into OneSpin's vision, mission, and solution development roadmap.
13:45 OneSpin Technical Deep Dive: Functional Correctness From Start to Finish
Nicolae Tusinschi, Product Specialist Design VerificationThe early elimination of bugs in an IC development process saves time and energy. This places pressure on component designers to perform more verification. However, given traditional simulation-based verification techniques, the ultimate result of this trend is designers spending more time creating stimulus and getting involved with overall verification, and less on creative design. Automated design code verification and functional analysis using automated apps allows for rapid design iterations along with comprehensive assertion-based verification. Combining with unique model-based mutation coverage, OneSpin’s functional correctness solution is crucial in today’s large and complex SOCs—this session delves into the particulars and looks ahead to what comes next.
14:30 User Case Study: Beyond Lint | ICsense
Cedric Walravens, Digital Team LeadManagers often see verification as a necessary evil that consumes an outlandish portion of the overall project effort. Any means to reduce the verification effort, therefore, should be grasped with both hands. Formal consistency checks are one such means. In addition to reducing effort, they can come extremely cheap in terms of engineering hours required. Key here is to provide a framework that enables designers to quickly check their designs before moving to any kind of simulation. In addition, a mechanism to create waivers that are not prone to code changes is necessary. Lastly, results must be reported concisively so that any unexpected changes are immediately spotted.
15:15 OneSpin Technical Deep Dive: FMEDA and Verification: A Symbiotic Relationship
Jörg Grosse, Product Manager Functional SafetyQuantitative FMEDA is crucial for compliance with ISO 26262. However, functional verification of safety mechanisms is at least as important. Are these two tasks truly independent? Can we leverage one to carry out the other? Yes, we can! Verification results can underpin assumptions that boost FMEDA metrics. On the other hand, modeling of the safety architecture may quickly reveal functional bugs, even without injecting faults. In this presentation, we explore both sides of the safety coin. Using examples extrapolated from real projects, we demonstrate how our customers have dramatically improved their hardware development flow.
16:00 User Case Study: Formal Verification of Safety Mechanisms | Infineon Technologies
Keerthikumara Devarajegowda, PhD CandidateThis talk will highlight how formal verification is deployed to exhaustively verify designs that implement safety mechanisms such as Error Correction Codes (ECCs). ECC designs that encode a large data vector and detect multiple bit errors have been traditionally verified with simulation-based methods even though they are better suited for formal verification. The main reason was the scalability of formal verification for large ECC designs. Properties that are written to verify large ECC designs time-out without an outcome owing to limited memory or time resources. We discovered that a succinct characteristic of ECC designs can be exploited to achieve an exhaustive proof on large ECC designs. For instance, the proof runtime of a 3 bit error detection/correction property requires less than 2 hours for passing on a 256 bit ECC design. Previously, the same property timed out after running for 6 days. We successfully applied this approach to multiple instances of ECC designs implemented across several safety-critical automotive SoCs. Results show that the proof runtime of the properties leveraging the proposed approach decreases at least by a factor of 50, and scales proportionally with the width of the data vector and detection and correction capability of the codes.
16:30 OneSpin Technical Deep Dive: Trust and Security: A Holistic Approach
John Hallman, Product Manager Trust & SecurityOneSpin's verification solutions bring a holistic approach to trust, assurance, and security issues by performing checks earlier in design verification phases. Technologies built upon world-class formal engines provide a great foundation for advanced integrity solutions. New apps methods include an automated assessment platform, structural and intelligent pattern detection, and new research into FPGA and SoC hardware/software co-verification techniques. In this presentation, users will see existing OneSpin solutions available today that address industry trust and security challenges and get a preview of new technologies needed to propel us forward against this rapidly growing problem.
17:15 User Case Study: Ensuring Completeness of Formal Verification with GapFree: To End or Not to End (Property Writing) | Sandia National Laboratories
Ratish Punnoose, Distinguished Member of Technical StaffA challenge with formal verification of RTL designs is knowing how much verification is enough. This is especially true when it comes to knowing when to stop writing additional properties. How can we achieve confidence that enough properties have been checked to verify the correctness of the design? OneSpin's GapFreeVerification methodology provides an answer to this problem. The methodology results in an automated check of the written properties to ensure that all design behaviors have been captured.
17:45 Closing Remarks and Preview of Day 2
OneSpin Master of Ceremonies
13:00 Welcome to Osmosis, Day 2
OneSpin Master of CeremoniesAgenda overview and event logistics
13:05 OneSpin Technical Deep Dive: Achieving RISC-V Integrity
Sven Beyer, Chief ScientistRISC-V is one of the hottest trends in the industry these days, with core providers from textbook open source to high-end commercial ones. The freedom to configure the RISC-V ISA in detail to the system needs, including custom instructions, is one of its strong appeals. However, this freedom comes with an equally great responsibility to assure integrity of the implemented RISC-V core, from ISA compliance over absence of hidden instructions or registers to absence of side-channel types of attacks. In this technical deep dive, we will take a look at OneSpin's current RISC-V apps for architecture and verification. We will also share some insight into the trust, assurance, and security RISC-V extensions planned for the upcoming OneSpin 360 2021.1 release.
13:50 User Case Study: Hardware Security Verification Using Unique Program Execution Checking | Technische Universität Kaiserslautern
Wolfgang Kunz, Professor, Department of Electrical & Computer EngineeringThe discovery of the Spectre and Meltdown security attacks in advanced processors has resulted in high public alertness about the security of hardware. The root cause of these attacks is information leakage across a new class of side channels, called transient execution side (TES) channels. Many sources believe that TES channels are intrinsic to highly advanced processor architectures based on speculation and out-of-order execution, suggesting that such security risks can be avoided by staying away from high-end processors. This talk, however, presents verification results involving OneSpin 360 DV, which show that the problem is of wider scope: similar leakages are possible also in average-complexity processors and must be addressed during RTL design time. Our new method is called Unique Program Execution Checking (UPEC). It does not require a priori knowledge on possible attacks and detects HW vulnerabilities systematically without demanding the clever thinking of a human attacker. UPEC provides a unified approach to HW security analysis. In addition to TES channels, it also detects those functional bugs in a design that cause security issues, for example, related to the communication between the core and its peripherals. We present results from several case studies on RISC-V systems, Rocket Chip, BOOM, Ariane, and Pulpissimo, in which UPEC detected a number of previously unknown security vulnerabilities.
14:20 OneSpin Technical Deep Dive: Assuring the Integrity of FPGA Designs
Vladislav Palfy, Director Application Engineering, and Sven Reimer, Senior Lead Software Engineer
Part 1: Avoid Systematic Design Errors from Synthesis Optimization
Systematic design errors introduced by automated design refinement tools, such as synthesis, can be hard to detect, not to mention damaging if they make it into the final device. Formal equivalence checking has been used for ASIC design flows for many years. As FPGAs become bigger, critical system components, exhaustively verifying the functional equivalence of register transfer level (RTL) code to synthesized netlists and the final placed-and-routed FPGA designs is mandatory.
Part 2: Overcome Obsolete FPGA Technology to Achieve Design Continuity
Many designs targeted to obsolete FPGAs are still functionally viable, but old FPGAs are no longer available to support the design or acquiring these obsolete FPGAs is cost prohibitive. The time, resources, and cost of redesigning onto newer FPGAs may not be practical. Re-synthesizing the RTL to meet the desired new technology may also not be feasible: there are many pitfalls associated with this process that can lead to errors finding their way into the design. Adding to the dilemma is the fact that new FPGA technology offers significant benefits that obsolete technology doesn’t have in terms of safety, security, trust, and power-saving features, while designs on obsolete technology can be inadequate to meet the stringent demands of today’s market. Retargeting these designs to newer FPGA technology extends the life of designs and ensures that designs are brought up to the latest safety and security standards while reducing power consumption. OneSpin’s FPGA Retargeting Solution can alleviate these challenges and effectively extend the lifespan of designs residing on old or obsolete FPGAs.
14:50 User Case Study: Large Counter Verification Using Semi-Formal Techniques | OneSpin on behalf of Nokia
David Landoll, Solutions Architect, OneSpin (Co-Author Kanthi Palaniappan, Specialist, SoC Verification, Mobile Broadband, Networks, Nokia)Formal verification is a powerful exhaustive verification tool that can significantly accelerate design verification and reduce verification risk. However, this exhaustiveness creates problems when the design being verified contains structures such as large counters. There are known techniques to perform “counter abstraction” which basically reduce the counter size, or remove it entirely from the design. For some designs, these techniques are adequate to enable formal verification to proceed. However, in our case, we needed to verify the actual counters themselves, so these abstraction techniques could not be used without altering the very design we were trying to verify. We needed a solution to the long runtimes and inconclusive results leaving the large counters unaltered. This presentation will cover the specifics of the large counter verification problem we faced, the various methods we considered, and the final approach we used to successfully verify the large counter corner cases throughout its full range of operation.
Move to Breakout Sessions
15:30 Breakout Sessions
Select the small group discussion topic that most appeals to you. You’ll have the opportunity to ask questions, share your thoughts, and bounce ideas off of others who are facing similar design and verification challenges.
Topic One: The Ins and Outs of Trust and Security
Discussion Moderators: John Hallman, Product Manager Trust & Security; Jörg Bormann, Formal Verification Specialist; and Sergio Marchese, Technical Marketing Manager, OneSpinThe modern world relies on complex electronic systems. Military, aerospace, automotive, and other critical infrastructure applications must all be resilient to adversary attacks that could compromise security, safety, and privacy. In the past, security engineering has focused on software and system-level issues, but there is ample evidence that ever more risks and attacks involve hardware, down to the microelectronic components. Embedded systems using relatively simple processors are not exempt. Malicious actors may construct misuse-case scenarios, exploit hardware weaknesses, and/or insert Trojans. Hardware assurance (HwA) is critical to build secure systems from the ground up. Join this breakout session to share your thoughts on the rapidly evolving landscape of trust, security, and assurance; discuss needs in verification and for emerging standards; and brainstorm ideas to solve complex problems on the horizon.
Topic Two: RISC-V and the Open Source Movement
Discussion Moderator: Sven Beyer, Chief Scientist, OneSpinThe RISC-V movement has opened up new frontiers of possibility and flexibility when it comes to processors. With great freedom comes great responsibility: to verify designs for ISA compliance, that is! RISC-V has the potential to be of significant benefit to military and aerospace designers, but exhaustive verification and proof of instruction set architecture compliance are essential. Join this breakout session to explore the far-reaching effects that RISC-V and the broader open source movement have had on electronics and to engage with others who are using RISC-V for a candid discussion of the best practices for incorporating open-source hardware into your designs.
Topic Three: FMEDA and Verification: Which Side Are You On?
Discussion Moderator: Jörg Grosse, Product Manager Functional Safety, OneSpinOur earlier presentation on functional safety showed why and how FMEDA and functional verification of safety mechanisms are symbiotic tasks. However, not all development flows and organizations take advantage of this. What are the challenges? Should safety and verification engineers work more closely together? Are there additional opportunities to mutually optimize the two processes? Join us to share your educated guesses, wild opinions, and experiences.
16:15 Breakout Session Summaries
Moderator from each breakout session will offer highlights and key takeaways from the discussion.
16:30 Closing Keynote Address: Application Specific ML: Building and Executing ML Models at Ultra-High Speeds with Applications in Debugging of SoCs
Claudionor José Nunes Coelho, VP/Fellow of AI - Head of AI Labs, Palo Alto NetworksWhile the quest for more accurate solutions is pushing deep learning research towards larger and more complex algorithms, edge devices with hard real-time constraints demand very efficient inference engines, e.g. with the reduction in model size, speed, and energy consumption. In this talk, we introduce a novel method for designing heterogeneously quantized versions of deep neural network models for minimum-energy, high-accuracy, nanosecond inference, and fully automated deployment on-chip. Our technique combines AutoML and QKeras (which is called AutoQKeras), combining layer hyperparameter selection and quantization optimization. Users can select among several optimization strategies, such as global optimization of network hyperparameters and quantizers, or splitting the optimization problems into smaller search problems to cope with search complexity. We have applied this design technique in several designs, including the event selection procedure in proton-proton collisions at the CERN Large Hadron Collider, where resources are strictly limited to hard-real time latency below 1 μs. Applications of ASML span over several applications, including the creation of high-level ML-enabled light posts that can be used in bug hunting or post-silicon debugging using formal technologies.
17:15 Closing Remarks
OneSpin Master of Ceremonies
Meet Our Speakers
Get to know our OneSpin 360 users and guest keynote speaker
Speakers are listed in order of appearance on the program
Cedric Walravens | ICsense
Digital Team Lead
Dr. ir. Cedric Walravens holds a PhD in Electrical and Electronics Engineering from the KU Leuven, Belgium. In 2012, he joined ICsense, the largest European fab-independent design group, where he currently occupies the position of Digital Team Lead. He is passionate about delivering consistent quality through a no-nonsense digital design flow, as well as growing knowledge within his team.
At Osmosis, Cedric will present a case study entitled Beyond Lint.
Keerthikumara Devarajegowda | Infineon Technologies
Keerthikumara Devarajegowda received his Master’s degree from Technische Universität Kaiserslautern, Germany, in the year 2016. He is currently with Infineon Technologies AG and is also pursuing his PhD at T.U. Kaiserslautern under the guidance of Dr. Wolfgang Ecker and Prof. Wolfgang Kunz. His research interests include formal verification, digital design modeling and automation techniques.
At Osmosis, Keerthi will present a case study entitled Formal Verification of Safety Mechanisms.
Ratish Punnoose | Sandia National Laboratories
Distinguished Member of Technical Staff
Dr. Ratish Punnoose is a Distinguished Member of Technical Staff at Sandia National Laboratories in Livermore, California. He provides technical leadership on the design and development of embedded systems for weapon components and has helped to incorporate formal verification as part of Sandia's digital design process. Ratish leads much of the formal verification of ASIC-based designs at Sandia. He is part of a group of Sandia researchers developing formal tools to specify system behavior and to create certifiably correct systems for high-consequence applications. Ratish has a PhD in Electrical and Computer Engineering from Carnegie Mellon University.
At Osmosis, Ratish will present a case study entitled Ensuring Completeness of Formal Verification with GapFree: To End or Not to End (Property Writing).
Wolfgang Kunz | Technische Universität Kaiserslautern
Professor, Department of Electrical & Computer Engineering
Wolfgang Kunz received the Dipl.-Ing. degree in Electrical Engineering from the University of Karlsruhe, Germany, in 1989 and the Dr.-Ing. degree in Electrical Engineering from the University of Hannover, Germany, in 1992. From 1993 to 1998, he was with Max Planck Society, Fault-Tolerant Computing Group at the University of Potsdam, Germany. From 1998 to 2001 he was a professor of Computer Science at the University of Frankfurt/Main. Since 2001 he is a professor at the Department of Electrical & Computer Engineering at Technische Universität Kaiserslautern.
Wolfgang Kunz conducts research in the area of system-on-chip design and verification. In many of his research projects, OneSpin Solutions has been a close collaboration partner. For his research activities Wolfgang Kunz has received several awards including the Berlin Brandenburg Academy of Science Award and the Award of the German IT Society. Wolfgang Kunz is a Fellow of the IEEE.
At Osmosis, Professor Kunz will present a case study entitled Hardware Security Verification Using Unique Program Execution Checking.
David Landoll | OneSpin Solutions on behalf of Nokia Corporation
David Landoll is a solutions architect at OneSpin Solutions, where he works to develop and deploy formal tools and methodologies. David focuses on safety, security, and trust related industries, including Department of Defense, automotive, and avionics. He has extensive experience in DO-254 and ISO 26262 safety standards and is a member of the North America DO-254 Users Group. With over 20 years of formal verification experience and almost 30 years of design and verification experience, David has directly managed and contributed to large projects, including an ADAS self-driving car system and safety-critical avionics SoCs, and has shared his expertise at numerous conferences and events. He holds a BSEE from the University of Arizona and MBA from Santa Clara University.
David has cultivated a strong working relationship with OneSpin's users at Nokia. At Osmosis, he will present a case study entitled Large Counter Verification Using Semi-Formal Techniques on behalf of co-author Kanthi Palaniappan, Specialist, SoC Verification, Mobile Broadband, Networks, Nokia.
Claudionor José Nunes Coelho | Palo Alto Networks
VP/Fellow for AI – Head of AI Labs
Claudionor N. Coelho is the VP/Fellow for AI – Head of AI Labs at Palo Alto Networks. Previously, he worked on Machine Learning/Deep Learning at Google. He is the creator of QKeras, a Deep Learning package for quantization on top of Keras with support for automatic quantization. He was the VP of Software Engineering, Machine Learning, and Deep Learning at NVXL Technology. He did seminal work on AI at Synopsys Inc, and he was the GM for Brazil for Cadence Design Systems, following the acquisition of Jasper Design Automation, where he was the Worldwide SVP of R&D. He has more than 80 papers, patents, academic, and industry awards. He is currently an Invited Professor for Deep Learning at Santa Clara University, and previously, he was an Associate Professor of Computer Science at UFMG, Brazil. He has a Ph.D. in EE/CS from Stanford University, an MBA from IBMEC Business School, and an MSCS and BSEE (summa cum laude) from UFMG, Brazil.
At Osmosis, Claudionor will deliver the closing keynote address on Day 2 on the topic of Application Specific ML: Building and Executing ML Models at Ultra-High Speeds with Applications in Debugging of SoCs.
Apply to Attend Osmosis 2020
Osmosis 2020 is a private event that is open primarily to current OneSpin users, but we have a limited number of registrations available for prospective users and other interested parties. You will receive an email confirmation containing registration information if your application is accepted.