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.
Formal Verification Applied to the Renesas MCU Design Platform Using the OneSpin Tools
Due to the wide range of different MCU types that are developed within a series of Renesas MCU’s in order to satisfy different applications we have developed the MCU-PF platform for both design and verification of a complete series of MCUs. A key issue is the effective verification for a combination of multiple IP components -this presents a significant task. Renesas developed the capability to use a Formal method of verification that provides full coverage of combinations of assertions while delivering significant reductions in both testing and verification time. Additional efficiency has been gained because the IP-Assertions are fully reusable along with the IP itself. This paper explains the methodology, its advantages and performance results compared to the simulation verification method.
Renesas is using 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.
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.
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.