Take a deeper look on how OneSpin 360 is applied and read our white papers
Achieving 100 % Functional Coverage by Operational Assertion-Based Verification
This white paper presents Operational Assertion-Based Verification (ABV), an advanced formal verification methodology resulting in a predictable, small number of high-level assertions capturing the functionality of a design. Operational ABV enables an automatic formal coverage analysis, which identifies holes in verification plans, unverified design functionality as well as errors and omissions in specifications. The formal coverage analysis ensures that 100 % of the design functionality is verified – answering the question 'Have I written enough assertions?'.
This white paper covers the 360 DV-Certify product.
Capturing Timing Diagrams in Operational SVA
Timing diagrams provide an excellent, intuitive starting point for writing assertions to capture the intended behavior of designs. However, the standard assertion languages SVA and PSL do not provide direct constructs for capturing timing diagrams. This white paper presents Operational SVA – a simple yet powerful SVA library – which allows to develop assertions directly from timing diagrams and waveforms.
This white paper covers the 360 DV-Verify product.
Formal Analysis of X Propagation
Verifying the absence of undefined signal values in a design is in general a hard problem. Formal 4-state logic analysis offers a powerful solution. This white paper discusses X-related verification issues, and how advanced 4-state formal analysis solves them. This white paper covers the 360 DV-Verify product.
Reducing Verification Risk with Formal-Based Observation Coverage
An effective measure of verification progress, together with guidance towards design areas remaining untested, requires a precise view of the test coverage achieved. To risk signing off the verification process without understanding the quality of testing raises the specter of post-production device bugs. OneSpin Solution’s patented Quantify technology employs Observation Coverage, which evaluates the effectiveness of a set of assertions being triggered by incorrect behavior in the design code.
Quantify Observation Coverage is available as part of the 360 DV-Verify product.
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.