Take a deeper look on how OneSpin 360 is applied and read our white papers
Check out our latest paper
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.