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.

Take a deeper look on how OneSpin 360 is applied and read our white papers


Check out our latest paper

Hierarchical Verification for EC-FPGA Flow

This document describes the methodology to apply EC-FPGA verification using hierarchical netlists. This approach is recommended in case the verification of the overall design has issues with convergence. The document contains a step-by-step description of different methods while providing reasoning for the soundness of each approach. It is assumed for this document that the reader is familiar with the basics of the equivalence checking process using OneSpin 360™ EC-FPGA™.

 

Sign up to access the white paper "Hierarchical Verification for EC-FPGA Flow"

SoC Verification from Pre-Fabrication to the Over-the-Air Update

The recent new of attacks on system infrastructures serves to highlight that hardware vulnerabilities in the supply chain are not only possible but inevitable if proper precautions are ignored. Verification throughout the entire supply chain is necessary to ensure the safety and security of hardware. Starting as early as the pre-fabrication stage, vulnerabilities, if left unchecked, can be an open invitation to malicious actions.
This paper provides a blueprint for how to combat vulnerabilities and weaknesses at the pre-fabrication level and beyond. Continuous verification of the hardware throughout the device lifecycle is key to ongoing prevention as well as the verification of over-the-air updates.

 

Sign up to access the white paper "SoC Verification from Pre-fabrication to  Over-the-Air Updates"

Capturing Timing Diagrams in Operational SVA

In order to formally verify design functionality, the intended behavior of the design under verification (DUV) must be captured in a formal language. Frequently, a specification document contains timing diagrams, which provide an excellent starting point for capturing the intended behavior of designs. However, the standard formal languages SVA and PSL, which are based on the paradigm of sequences (SEREs = Sequential Extended Regular Expressions), do not provide direct constructs for capturing timing diagrams.

This paper presents the language constructs required for easily deriving properties from timing diagrams and waveforms, and their implementation in OneSpin's Operational SVA

Sign up to access the white paper "Capturing Timing Diagrams in SVA"

Reducing Verification Risk with Formal-Based Observation Coverage

Ensuring an Integrated Circuit (IC) has been effectively tested during the verification process prior to fabrication remains a significant issue for electronics design teams. This is made worse by an inability to effectively measure verification progress. Various verification coverage techniques have been employed for this task, but they all exhibit certain drawbacks.

This paper discusses the coverage issue and current solutions, including methods for their improvement, before exploring the notion of Observation Coverage, a technique demonstrating significant promise as an effective verification closure metric. The paper goes on to introduce Quantify™ Observation Coverage, a new, formal-based approach to coverage measurement that has been proven on real designs to increase verification confidence significantly. A discussion of this technique, its use on real designs, employed use models and verification flow integration are also included in the paper.

Sign up to access the white paper "Trust Assurance and Security Verification of  Semiconductor IPs and ICs"

Trust Assurance and Security Verification of Semiconductor IPs and ICs

Connected autonomous vehicles, 5G networks, Internet-of-things (IoT) devices, defense systems, and critical infrastructure use ASIC and FPGA SoCs running artificial intelligence algorithms or other complex software stacks. Vulnerable or tampered ICs can compromise the safety of people and the confidentiality, integrity, and availability of sensitive information.

This paper analyzes the trust and security risks in the pre-silicon chip development flow, and considers the industry standards and EDA solutions to address those risks. The target audience includes semiconductor executives, engineering managers, and security experts.

Sign up to access the white paper "Trust Assurance and Security Verification of  Semiconductor IPs and ICs"

Trust Assurance and Security Verification of Semiconductor IPs and ICs: Part 2

Connected autonomous vehicles, 5G networks, Internet-of-things (IoT) devices, defense systems, and critical infrastructure use ASIC and FPGA SoCs running artificial intelligence algorithms or other complex software stacks. Vulnerable or tampered ICs can compromise the safety of people and the confidentiality, integrity, and availability of sensitive information.

This paper analyzes the trust and security risks in the pre-silicon chip development flow, and considers the industry standards and EDA solutions to address those risks. The target audience includes semiconductor executives, engineering managers, and security experts.

Part 2: Side channels, vulnerabilities, security bugs

Sign up to access the white paper "Trust Assurance and Security Verification of  Semiconductor IPs and ICs"

Assuring the Integrity of RISC-V Cores and SoCs

The open RISC-V processor architecture is shaking up the intellectual property (IP) and system-on-chip (SoC) worlds. There is great interest and much industry activity underway. However, successful RISC-V core providers will have to verify all aspects of integrity for their designs: functional correctness, safety, security, and trust. SOC developers evaluating potential RISC-V need to check that their standards for design integrity are fully satisfied. They may wish to re-run the core-level verification steps and then perform additional tasks to ensure that the cores have been integrated properly. Verification of RISC-V designs is especially challenging because of optional features, implementation flexibility, and provisions for customer extensions.

This paper presents the OneSpin RISC-V Integrity Verification Solution and discussed how its components verify all four aspects of design integrity at both the processor core and full-chip levels. It concludes by detailing some issues found by the OneSpin Solution on RISC-V core and SoC designs available as open source.

Sign up to access the white paper "Assuring the Integrity of RISC-V Cores and  SoCs"

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 GOMACTech Conference paper "Complete Formal Verification of  RISC V Processor IPs for Trojan-Free Trusted ICs"

Design Verification Is All About Good Hygiene

Design verification has a lot in common with human hygiene practices. The goal of both activities is to remove all dirt, grime, and bugs through an active process of establishing good hygiene. If this process is not followed properly, the result is viruses, infections, and other illnesses. Good verification hygiene is as important in semiconductor development as human hygiene is for a healthy body. This white paper discusses the different stages of verification hygiene and what kind of issues can be detected and corrected at each stage. Any design change requires it to be sanitized to eliminate any bugs introduced. A rinsing phase can detect more serious problems, while a deep scrub of the design removes corner-case bugs.

Download white paper Design Verification Is All About Good Hygiene

Formal Verification of Floating-Point Hardware with Assertion-Based VIP

Hardware for integer or fixed-point arithmetic is relatively simple to design, at least at the register-transfer level. If the range of values and precision that can be represented with these formats is not sufficient for the target application, floating-point hardware might be required. Unfortunately, floating-point units are complex to design, and notoriously challenging to verify. Since the famous 1994 Intel Pentium bug, many companies have investigated and successfully applied formal methods to this task. However, solutions often rely on a mix of the following: hard-to-use formal tools; highly specialized engineering skills; availability of a suitable executable model of the hardware; and significant, design-specific engineering effort. In this paper, we present an alternative floating-point hardware verification approach based on a reusable, IEEE 754 compliant SystemVerilog arithmetic library. While not addressing all verification challenges, this method enables engineers to set up a formal testbench and uncover deep corner-case bugs with minimal effort. Results from industrial applications are reported.

Sign up to access the DVCon China paper "Formal Verification of Floating-Point  Hardware with Assertion-Based VIP"

ISO 26262:2018 Fault Analysis in Safety Mechanisms

ISO 26262-5 requires the determination of hardware safety metrics, including SPFM and LFM. Latent and residual diagnostic coverage are also important metrics to assess the effectiveness of safety mechanisms. Achieving ASIL-B, ASIL-C or ASIL-D compliance is challenging, and requires a detailed analysis of faults in the safety mechanisms. This paper introduces a systematic, largely automated process to compute safety metrics. It covers accurate fault analysis in safety mechanisms with and without error-correcting capabilities. The approach scales to large SoCs, provides accurate results, and significantly reduces the need for manual analysis and fault simulation. Experiences and results of its application to a number of gate-level netlist designs are reported.

Sign up to access the DVCon Europe paper "ISO 26262:2018 Fault Analysis in  Safety Mechanisms"

OneSpin Formal Solutions for SystemC/C++ Verification

OneSpin Solutions provides its popular 360 DV™ formal verification product line, which allows for both the automated checking and full assertion-based verification of SystemC/C++ design representations. This solution extends the verification capability that may be applied to abstract designs, coded in SystemC/C++ for many different use models.

This white paper describes the OneSpin solution and explains how it accelerates and improves verification of SystemC/C++ designs.

Sign up to access the white paper "OneSpin Formal Solutions for SystemC/C++  Verification"

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 DVCon China Conference paper "Scaling Formal Connectivity Checking to  Multi-Billion-Gate SoCs with Specification Automation"

Shifting the Burden of Tool Safety Compliance from Users to Vendors

Functional safety standards demand that this risk be assessed and adequately minimized through tool qualification and other processes. For engineering teams, this is a time-consuming task and, worryingly, one for which there are no mature solutions yet. Tool vendors may provide safety certificates or packages, in an attempt to support their customers with safety compliance. Strategies vary and so do the benefits to the user and project.

In this paper, we review requirements on tool classification and qualification, present different safety compliance strategies, and explain their benefits to safety-critical hardware projects.

Download white paper Shifting the Burden of Tool Safety Compliance from Users  to Vendors

The Rise and Fall of Synthesis Bugs in Safety-Critical FPGAs

Functional safety standards require a rigorous development process to minimize the risk of introducing systematic faults. Some RTL issues may only reveal themselves as bugs in the synthesis netlist. Additionally, synthesis tools manipulate the design to map it into the fixed FPGA structure. These complex transformations present a high risk of introducing bugs. Gate-level simulation and lab testing can only cover a tiny portion of the FPGA functionality and are likely to miss implementation bugs. Moreover, they are slow to run and challenging to debug. 

This white paper presents an implementation signoff flow proving that the final FPGA netlist is functionally equivalent to the RTL model. Based on FPGA-specific, mature formal verification technology, the solution is exhaustive and efficient, catching many issues before synthesis starts.

Download white paper The Rise and Fall of Synthesis Bugs in Safety-Critical  FPGAs

Using Formal to Verify Safety-Critical Hardware for ISO 26262

Automotive technology has come a long way since the days of the Ford Model T. Today's smart vehicles not only assist their drivers with tasks such as parking, lane management, and braking, but also function as a home away from home, with WiFi hotspots and sophisticated entertainment systems. These sophisticated features are made possible by increasingly complex electronic systems—systems that present countless new opportunities for things to go wrong. A defective headrest video screen may be an irritation to a young passenger in the back seat, but a malfunctioning corrective steering system could cost the occupants of the vehicle their lives. Adequate verification is essential.

OneSpin's formal verification solutions can help automotive suppliers continue to advance their technology while keeping drivers and passengers safe. Our safety-critical white paper examines the ISO 26262 automotive standard and makes a case for its indispensability.

Download white paper Using Formal to Verify Safety-Critical Hardware for ISO  26262

When correct is not enough – Formal verification of fault-tolerant hardware

Fault-tolerant hardware development is no longer a niche and presents new challenges. Many engineers face the daunting task of having to examine countless faulty variants of their design in order to integrate and verify multiple safety mechanisms within complex Systems-on-Chip (SoCs).

This white paper examines key goals and challenges in fault-tolerant hardware verification, and presents formal solutions that ensure predictable hardware behavior under all relevant operating conditions and fault scenarios, while saving in engineering and computational resources. 

Download white paper When correct is not enough – Formal verification of  fault-tolerant hardware

Get inside OneSpin and download our technical materials