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