PRODUCTS 360 MV

The OneSpin 360® MV Product Family
Most Comprehensive Formal Assertion-Based Verification

Datasheet, articles and white papers about 360 MV
Press coverage 360 MV

Overview

OneSpin's 360 MV product family is the most comprehensive formal assertion-based verification (ABV) solution for RTL designs. It is the only verification solution in the industry providing an exhaustive coverage analysis. This enables users to consistently find intricate design errors missed by other approaches – confirmed in more than 300 verification projects.
360 MV covers the broadest range of formal ABV applications for formal verification starters, experienced users and experts – from fully automatic RTL checks all the way to OneSpin's patented, highest quality gap-free verification. It guides design, verification and integration engineers in choosing the best approach – simulation or formal techniques – giving users full control over the right verification effort/quality mix for their design and project schedule.

Formal ABV 360 MV has powerful support for standard formal ABV applications – such as automatic RTL checks, implementation intent verification, and verification of end-to-end functional requirements – and extends them with a unique Operational ABV methodology.
Operational ABV simplifies verification planning, eases assertion writing working from timing diagrams and is the key for an exhaustive coverage analysis ensuring no design behavior is missed during verification. The exhaustive coverage analysis automatically uncovers holes in the verification plan, detects unverified design functionality, and finds errors and omissions in design specifications. It generates diagnosis information guiding the user in writing additional assertions to close verification holes.
Operational ABV and 360 MV's coverage analysis are key enhancements that enable the efficient, gap-free verification of critical modules and IP – delivering verification productivity and confidence that cannot be ensured by any other functional verification approach today.

360 MV's comprehensive spectrum of formal ABV applications enables step-by-step learning and adoption of formal ABV techniques, allowing new users to become productive in days. At every level, assertions are exhaustively verified – equivalent to running and checking every possible simulation trace of a design. It requires no input stimuli, so verification can start weeks or months before testbenches become available. Proven assertions can be reused in system-level testbenches as coverage points, or to speed integration verification.

Highlights

  • Automatically uncovers verification holes, finding the bugs that are missed by other tools
  • Enables highest possible block/IP quality through Operational ABV and exhaustive coverage analysis
  • Confirms 'no more verification holes' – user knows when verification is 'done'
  • Guides and eases assertion development working from timing diagrams
  • Wide range of formal ABV applications, adapting to project requirements and available expertise
  • Seamless learning and adoption makes new users productive in days

Operational ABV Plus Formal Coverage Analysis

Standard Formal ABV provides a wide range of applications for both starters and experienced users to verify design aspects early and with high productivity. However, there is no approach to know when enough assertions have been written and which verification holes are left, allowing bugs to escape verification. Operational ABV plus 360 MV removes this risk and uncertainty.
The Operational ABV methodology guides users in writing SystemVerilog assertions (SVA) that capture the intended behavior of specified design operations such as the read and write operations of a cache controller. The methodology provides an SVA modeling layer – called OperationalSVA™ – that enables operational assertions to be written directly from timing diagrams that describe the intended behavior of operations. Operational assertions – in contrast to 'arbitrary' assertions as in standard ABV – enable an exhaustive coverage analysis which determines whether all design behavior is captured by a set of operational assertions.
This analysis automatically uncovers any verification holes, guides the user in writing additional assertions to close the holes and tells the user when verification is 'done'. More than 300 completed IP and module verifications confirm that this approach consistently detects the design errors missed by other verification approaches – and achieves both certified full functional coverage (see Fig. 2) and highest possible design confidence. The resulting module/IP quality significantly reduces time-consuming error-correction loops during integration-level and chip-level verification as well as respins. The approach is also key to systematically reverse engineer and safely redesign legacy IP.

Verification holes

The 360 MV Product Family

The modular 360 MV product family comprises five integrated products (see Figure 3) that cover the application levels shown in Figure 1. Each step up in the product family extends previous products with new features that increase verification productivity and coverage.

360 MV Inspect™ performs an extensive set of fully automatic formal checks to detect RTL errors as soon as first code is available, enabling an early, fast sanity check and code clean-up that reduces late stage debug iterations.

360 MV Check™ enables exhaustive verification of micro-architecture and implementation aspects using simple assertions to detect implementation bugs earlier and faster than using simulation, resulting in cleaner blocks, earlier system integration and faster system simulation bring-up.

360 MV Verify™ provides the capacity and performance to exhaustively verify end-to-end block-level functional requirements to find deep, intricate errors that are hard to find using simulation. It is also the entry point for Operational ABV.

360 MV Assure™ extends 360 MV Verify and the Operational ABV methodology by a formal coverage check that automatically uncovers input scenarios that lead to yet unverified design behaviors. A diagnosis environment guides users in writing additional assertions to close these verification holes.

360 MV Certify™ implements OneSpin's GapFree-Verification™ process – based on Operational ABV and a complete set of formal coverage checks – which guides users through all phases of verification planning, assertion writing, and automatic detection of all verification holes to achieve a gap-free formal verification of the design's full functionality.
debug

Product Interoperability

All 360 MV products are integrated in the same verification environment featuring, among others, frontends for Verilog, SystemVerilog and VHDL; fully-fledged mixed-language support and optional generation of multi-valued models; a collection of powerful proof engines; parallel execution including LSF support; programmable Tcl shell; assertion development environments; comprehensive root cause analysis framework that significantly eases and speeds assertion and RTL debugging; automatic proof-status management; on-the-fly adding of constraints without recompilation; and more.

Click here to download Datasheet.