close By using this website, you agree to the use of cookies. Detailed information on the use of cookies on this website can be obtained on OneSpin's Privacy Policy. At this point you may also object to the use of cookies and adjust the browser settings accordingly.

Conference Materials

Access the latest materials our verification experts presented at industry conferences.

DAC 2020: Automated Trustworthiness Assessment of Third-Party Semiconductor IPs

IP Track Paper Presented by John Hallman, Product Manager Trust & Security

Developers of safety- and security-critical SoCs can no longer afford to ignore the risks of security vulnerabilities when integrating third-party IPs. Re-verification of an IP is not feasible, and the cost is prohibitive, even more so when the implementation-level expertise is not in-house. Verification and code reviews are likely to miss stealthy Trojans or vulnerabilities that surface in deep corner-case, misuse scenarios that are far from the IP intended usage. Some solutions are emerging to address these challenges. The Aerospace Corporation and OneSpin will share results of the application of an automated IP trust and assurance flow on over 90 RTL designs.

Sign up to access the GOMAC Conference paper "Complete Formal Verification of  RISC V Processor IPs for Trojan-Free Trusted ICs"

DAC 2020: Security and Trust Assurance of RISC-V Open-Source Cores

Poster Session presented by Sven Beyer, Chief Scientist, OneSpin Solutions

RISC-V has reinvigorated the open-source hardware community. Many individuals, companies, and organizations, including the OpenHW Group, are continuously releasing new and updated implementations of the RISC-V ISA. However, thorough functional verification of processors is very costly. Established IP providers using proprietary architectures have decades of experience and enormous resources dedicated to functional verification. And yet, security issues are routinely missed. RISC-V makes it possible and affordable to take the assurance and security verification of processor cores to the next level, matching or even exceeding the quality of established IP providers. Edaptive Computing and OneSpin will share results of the application of a RISC-V formal verification solution to two cores (RocketCore and OpenHW CV32E40P).

Sign up to access the GOMAC Conference paper "Complete Formal Verification of  RISC V Processor IPs for Trojan-Free Trusted ICs"

DAC 2020: Analysis of Faults in Safety Mechanisms and Computation of ISO 26262 Metrics

Poster Session presented by Jörg Grosse, Functional Safety Product Manager, OneSpin Solutions

Quantitative FMEDA for automotive applications and compliance with ISO 26262 can be challenging. Fault injection can be used for deriving hardware safety metrics. However, for complex chips or semiconductor IPs with a variety of safety mechanisms, using fault simulation is laborious and time-consuming. What are the right stimuli to use? How can I speed up fault simulation? How can I detect early in the flow if the safety architecture will not get me to the target SPFM and LFM metrics, whether my goal is an ASIL-B, ASIL-C, or ASIL-D system? The good news is that there are alternative ways to approach the problem that can reduce or even eliminate the need for fault simulation. Discover how to implement a streamlined, automated, and efficient quantitative FMEDA flow.

Sign up to access the GOMAC Conference paper "Complete Formal Verification of  RISC V Processor IPs for Trojan-Free Trusted ICs"

DAC 2020: The Role of Equivalence Checking for FPGAs in Nuclear Applications

Poster Session presented by Jürgen Dennerlein, Platform Architect & Hardware Developer, Framatome

The IEC SC 45A standard series regulates electronic instrumentation and control equipment in nuclear applications. In particular, IEC 62566 focuses on FPGA development activities, including verification of the post-synthesis and post-place-and-route netlists. How can you reduce the need for slow gate-level simulations? How can you be sure that the implementation tools have not introduced errors? Is that possible when using more advanced implementation flows? Luckily, there are formal verification tools that are dedicated to FPGA flows. Within a few days of effort, it is possible to exhaustive verify large netlists. Crucially, these tools are independent of the implementation tools, an essential requirement from safety standards.

Sign up to access the GOMAC Conference paper "Complete Formal Verification of  RISC V Processor IPs for Trojan-Free Trusted ICs"

DAC 2020: Formal Verification of RISC-V Cores

RISC-V Theater Presentation by Salaheddin Hetalani, OneSpin Field Application Engineer

OneSpin is a proud member of RISC-V International and the OpenHW Group. As part of our participation in the Virtual DAC RISC-V Pavilion, FAE Salaheddin Hetalani will give an overview of how formal verification offers critical advantages when it comes to ensuring that designs incorporating open source hardware are free of bugs and other issues. Featured in the presentation are a number of case studies involving successful verifications with OneSpin's RISC-V Verification App, which automates and accelerates verification to ensure proof of compliance to the RISC-V instruction set architacture (ISA) with no gaps or inconsistencies.

Sign up to access the GOMAC Conference paper "Complete Formal Verification of  RISC V Processor IPs for Trojan-Free Trusted ICs"

Complete Formal Verification of RISC-V Processor IPs for Trojan-Free Trusted ICs

RISC-V processor IPs are increasingly being integrated into system-on-chip designs for a variety of applications. However, there is still a lack of dedicated functional verification solutions supporting high-integrity, trusted integrated circuits. This paper examines an efficient, novel, formal-based RISC-V processor verification methodology. The RISC-V ISA is formalized in a set of Operational SystemVerilog assertions. Each assertion is formally verified against the processor’s RTL model. Crucially, the set of assertions is then mathematically proven to be complete and free from gaps, thus ensuring that all possible RTL behaviors have been examined. This systematic verification process detects both deliberate hardware Trojans and genuine functional errors present in the RTL code. The solution is demonstrated on an open-source RISC-V implementation using a commercially available formal tool, and is arguably a significant improvement to previously published RISC-V ISA verification approaches, advancing hardware assurance and trust of RISC-V based designs. 

Sign up to access the conference paper "Complete Formal Verification of RISC-V  Processor IPs for Trojan-Free Trusted ICs"

Scaling Formal Connectivity Checking to Multi-Billion-Gate SoCs with Specification Automation

Connectivity checking is a popular formal verification application. Formal tools can automatically generate assertions using a specification table as input and prove them exhaustively. Simulation-based verification, on the other hand, requires significantly more effort while providing a fraction of the coverage. However, chip complexity is rapidly increasing. ASICs and FPGAs for heterogeneous computing, 5G, AI, and ML applications have hundreds of thousands of deep connections to verify. The computational challenge is enormous. Furthermore, creating the connectivity specification is a time-consuming, error-prone task. The most recent papers on formal connectivity checking report results on designs of up to 200 million gates, with up to 132 thousand connections proven. This paper presents an innovative approach to addresses both specification and computational challenges, and scale formal connectivity checking to previously intractable problems. Results are reported on a multi-billion-gate SoC fabric in the latest technology node with over 1 million connections to specify and verify.

Sign up to access the conference paper "Scaling Formal Connectivity Checking to  Multi-Billion-Gate SoCs with Specification Automation"

Complete Formal Verification of a Family of Automotive DSPs

Formal verification becomes the method of choice for designs with stringent quality requirements. For complex architectures with many implementation alternatives, however, the development and maintenance of complete formal specifications remains a challenge. In this work, we present an efficient semi-formal specification approach for processor designs with a large number of architectural variants.

Sign up to access the conference paper "Complete Formal Verification of a  Family of Automotive DSPs"

Complete Formal Verification of TriCore2 and Other Processors

This paper describes an innovative and powerful methodology for the complete formal verification of modules and intellectual property (IP), and its application to the verification of processor IP. Unlike other formal approaches, the methodology is a self-contained approach to hardware verification, independent of simulation.

Sign up to access the conference paper "Complete Formal Verification of  TriCore2 and Other Processors"

Get inside OneSpin and download our technical materials