13:00 Welcome to Osmosis, Day 1

OneSpin Master of Ceremonies

Agenda overview and event logistics

13:05 Keynote Address: What OneSpin's Acquisition by Siemens Means For Formal Verification—and Users Like You

Ravi Subramanian, Senior Vice President and General Manager, and Raik Brinkmann, Senior Director of Engineering, Siemens Digital Industries Software

In May 2021, OneSpin Solutions was acquired by Siemens Digital Industries Software, combining OneSpin’s solutions for key growth markets—including Trust and Security, Safety, RISC-V, and FPGAs—with Siemens' Questa Formal products and expertise. The OneSpin 360™ formal platform bolsters a cohesive and comprehensive Siemens EDA verification solution spanning simulation, formal, emulation, and prototyping.

In this keynote presentation, Siemens EDA VP Ravi Subramanian and “new” Siemens EDA leader Raik Brinkmann (former CEO of OneSpin) offer behind-the-scenes insight into what the acquisition means for the future of formal technology—and the myriad ways that end-users will benefit.

13:35 OneSpin Technical Deep Dive: Functional Correctness: Don't Let It Bug You!

Nicolae Tusinschi, Senior Field Application Engineer

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:20 User Case Study: Merging Formal and Simulation Verification Metrics Using OneSpin 360™ | Xilinx, Inc.

Pradeep Valipe, Senior Staff Design Engineer

Formal- and simulation-based verification are two mainstream solutions for signing off verification. Increasing the footprint of formal in verification requires flows to be able to measure the contribution of formal towards verification signoff in conjunction with traditional simulation-based environments. Typical metrics used for verification signoff are code and functional coverage. This paper discusses a flow that merges both code and functional coverage contributions of formal and simulations, thereby reducing the duplication of verification effort and reducing overall verification signoff time.

14:50 User Case Study: PortableCoverage: Bringing Formal Results into vManager | ams OSRAM

Sujith Antony Koyan Paulose, Senior Staff Engineer (Digital Verification)

Simulation and formal verification are core technologies to chip design verification strategy, where formal is now an increasing part of the mainstream flow and needs to be integrated with simulation-based tools. In this presentation, we will discuss a use case on how integration between simulation and OneSpin 360™ functional and structural metrics is carried out, and how visualization of metrics from several sources is made possible in vManager.

15:20 10-Minute Break

15:30 User Case Study: Floating-Point Unit Formal Verification | Xilinx, Inc.

Parag Rao, Senior Design Verification Engineer

Floating-point operations are data-sensitive in nature. Achieving full data proof using functional verification is an arduous task. Our team at Xilinx chose OneSpin’s Floating-Point Unit (FPU) formal solution to get full proof with no constraints in all the applicable modes. OneSpin has implemented the VFMA complex function and provides a debugger with floating-point awareness. With the OneSpin 360™ tool, we achieved full proof verification on floating-point VADD.fp, VSUB.fp, Compare and Conversion operations, and achieved good coverage on VMUL.fp and VMAC.fp operations by restricting the number of multiplier inputs. We look forward to sharing our approach and results with colleagues across the industry.

16:00 OneSpin Technical Deep Dive: Varied Approaches to Verification of FPGA Designs

Sven Reimer, Software Engineer Manager Equivalence Checking

This technical deep dive is a three-part crash course on OneSpin's FPGA-related solutions and apps.

Part 1: Equivalence Checking for FPGA

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. OneSpin 360 EC-FPGA is indispensable for achieving such verification goals.

Part 2: FPGA Retargeting

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

Part 3: FPGA User Case Studies and Success Stories

OneSpin 360 users around the world are achieving their verification goals with FPGA retargeting and equivalence checking. In this segment of the session, we summarize several success stories and case studies from our customers.

16:30 OneSpin Technical Deep Dive: Making Full Use of Custom RISC-V Extensions with Automated Verification

Sven Beyer, Program Manager, Processor Verification

RISC-V continues to be one of the hottest trends in the industry, 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 to absence of hidden instructions or registers. We will highlight how cores with custom instructions and custom registers can be formally verified with a high degree of automation given a machine readable description of the custom extensions.

17:15 Roundtable Discussion and Questions

An open forum to ask any final questions of our speakers and/or raise topics for discussion

17:25 Closing Remarks

OneSpin Master of Ceremonies

13:00 Welcome to Osmosis, Day 2

OneSpin Master of Ceremonies

Agenda overview and event logistics

13:05 Keynote: Expanding the Reach of Formal

Raik Brinkmann, Senior Director of Engineering, Siemens Digital Industries Software

During his tenure as CEO of OneSpin, Raik Brinkmann placed the highest priority on the continuous innovation and progress of formal verification technology. His belief that the benefits of formal technology can be applied to a vast range of verification application areas is evident in the broad and widely adopted family of OneSpin solutions: solutions that have assured the functional correctness, safety, trust, and security of designs across the globe.

In his Osmosis keynote address, Raik offers a guided look behind the scenes at the many ways OneSpin: A Siemens Business continues to push the boundaries of formal verification through:

– Research with higher education institutions and government entities

– Open-source initiatives like RISC-V

– Scalability of formal verification technology and methodology

Learn more about how OneSpin technology will continue to impact the expanding reach of formal with the goal of enabling engineers everywhere to achieve the highest degree of IC integrity in their designs.

13:30 OneSpin Technical Deep Dive: Introduction to Safety Architecture Modeling

Jörg Grosse, Program Manager Functional Safety

Failure modes, effects, and diagnostic analysis (FMEDA) is an analytical method to assess an IC's safety architecture and implementation. In this session, we introduce the concept of safety architecture modeling based on safety feature templates. We further explain how the safety architecture model can be mapped to complex IPs and SoCs to perform a safety analysis and automate the FMEDA steps, while significantly reducing fault simulation requirements compared to traditional FMEDA flows.

14:00 User Case Study: Complex FMEDA Made Simple | Kalray

Jehan-Philippe (JP) Barbiero, Hardware Verification Manager

Large designs run into the limits of traditional functional FMEDA. The cost in engineering effort, both to perform complex functional safety analysis and to conduct time-consuming fault simulation, are major industry pain points. Kalray and OneSpin have co-developed an EDA methodology that turns complex functional safety analysis into a relatively simple structural safety analysis. Kalray automated FMEDA on our flagship Intelligent Massively Parallel Processor Array, at RTL level. This approach has solved many of the challenges in complex FMEDA and we are excited to share our experience with industry colleagues.

14:30 OneSpin Technical Deep Dive: Leveraging the Power of Formal For SystemC/C++

Vlada Kalinic, Product Specialist SystemC

This session introduces you to our formal solution for verification of SystemC/C++ designs. We then examine a case study from MaxLinear, in which we dive into how the company has implemented the solution and explore the results they have achieved.

The use of C and C++ for describing electronic hardware components, particularly at the algorithmic level, has been commonplace for many years. The advent of the SystemC standard, which layered a set of hardware and system design features on top of C++, through the use of a C++ class library, has made it easier to specify hardware components in the software focused language. High-level synthesis (HLS) transforms algorithmic and potentially untimed design models, often written in SystemC and C++, to fully timed RTL design blocks. HLS tools are particularly popular as a method to rapidly generate design components with varying microarchitectures, while optimizing algorithm processing datapaths rapidly and effectively.

15:00 User Case Study: Formal Verification of SystemC Designs | MaxLinear

Gordon Cheung, Technical Director

Due to the limited availability of SystemC tools, much of the verification task is performed on the resulting synthesized RTL code, introducing a level of indirection that makes correcting issues at the SystemC/C++ level complex and time consuming. In addition, artifacts of the SystemC standard, including the lack of an unknown, or X, state and potential race conditions between threads, result in further ambiguity that must be eliminated before synthesis. In this presentation, we explore a formal app to fully verify SystemC/C++ designs and analyze the results we have achieved with OneSpin 360 DV-Inspect for SystemC.

15:30 10-Minute Break

15:40 OneSpin Technical Deep Dive: Verification For a More Secure Tomorrow

John Hallman, Product Manager Trust & Security

Cyberattacks continue to dominate news headlines, and attacks now target not only the software, but also the supply chain and the underlying hardware including the integrated circuits (IC). Compared to software, ICs are much more difficult and costly to patch once fielded—therefore, early identification of potential vulnerabilities is increasingly important.

In this presentation, we will discuss OneSpin 360™ formal verification tools and methods for early security verification on both modules of intellectual property (IP) intended for integration into an IC and on the IC itself. We will also show how these methods fit into broader standards efforts and other related work amongst the Siemens team. With the cooperative efforts from all of these teams, we will achieve better security practices early and throughout development, manufacture, and integration, in turn making our end products and systems more secure for end customers.

16:25 User Case Study: Evaluating Capabilities for Assurance of Third Party Intellectual Property | Sandia National Laboratories

Vivian Guzman Kammler, Technical Program Lead, Embedded Systems Analysis

High levels of verification rigor and analyzability are sacrosanct when designing high consequence systems abiding by always-never principles. Reliance on third party suppliers to meet mission objectives must be balanced with the provision of data artifacts and introspection for assurance, safety, and security. Ms. Kammler's team was tasked to evaluate the state of commercial capabilities for assurance of third party intellectual property. In this talk, she will share how OneSpin utilities fit into this evaluation and opportunities to further support programs facing these assurance challenges.

16:55 Roundtable Discussion and Questions

An open forum to ask any final questions of our speakers and/or raise topics for discussion

17:15 Closing Remarks

OneSpin Master of Ceremonies