13:00 Welcome to Osmosis, Day 1

OneSpin Master of Ceremonies

Agenda overview and event logistics

13:05 Opening Keynote Address: IC Integrity in Today's Evolving World

Raik Brinkmann, President & CEO, OneSpin

When 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 Verification

The 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 Lead

Managers 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:00 Break

15:15 OneSpin Technical Deep Dive: FMEDA and Verification: A Symbiotic Relationship

Jörg Grosse, Product Manager Functional Safety

Quantitative 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 Candidate

This 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 & Security

OneSpin'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 Staff

A 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 Ceremonies

Agenda overview and event logistics

13:05 OneSpin Technical Deep Dive: Achieving RISC-V Integrity

Sven Beyer, Chief Scientist

RISC-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 Engineering

The 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.

15:20 Break

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, OneSpin

The 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, OneSpin

The 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, OneSpin

Our 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 Networks

While 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