SOLUTIONS360 MV

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

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

Highlights

  • Provides the most comprehensive formal assertion-based verification solution for RTL designs
  • Covers a broad range of use-cases for both newcomers and experienced users
  • Slashes verification effort by up to 10X compared to simulation
  • Guides and eases assertion development working from waveforms and timing diagrams
  • Enables highest quality through automatic detection of verification gaps
  • Scales for designs where other formal tools fail to deliver results
  • Step-by-step learning and adoption approach makes new users productive in days

Overview

Formal ABV OneSpin's 360 MV product family is the most comprehensive formal assertion-based verification (ABV) solution for RTL designs available today. It covers a wide range of use-cases and verification tasks for both newcomers and experienced users, employing standard assertion languages like SystemVerilog Assertions (SVA) and the Open Verification Library (OVL).
It guides design and verification engineers in choosing the best approach – simulation or formal techniques – for exploring and verifying RTL designs to save up to 10x in verification effort, to shorten verification schedules and to achieve significantly higher design quality.
The 360 MV product family delivers the capacity and performance to cover a multitude of use-cases, from fully automatic RTL checks for large designs all the way to OneSpin's patented, highest quality gap-free verification. It provides entry points for both newcomers and experienced users and gives the user full control over the best verification effort/quality mix for the design and project schedule.

360 MV supports the 'standard' formal ABV applications – automatic RTL checks, implementation intent verification and verification of functional requirements – and extends them with unique, systematic verification of design operations (see Figure 1).
This operation-based verification approach allows engineers to develop assertions from waveforms and timing diagrams – concepts familiar from simulation. This link to simulation eases learning, verification planning and correlation of coverage information from simulation and 360 MV.
360 MV's operation-based approach also features automatic detection of verification gaps in SVA assertion sets and OneSpin's GapFreeVerification™ process to achieve design quality – for mission-critical IP, for example – that cannot be ensured by any other verification approach today.
360 MV's comprehensive spectrum of use-cases and application levels enables step-by-step learning and adoption 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. No input stimuli are needed, so verification can start weeks or months before testbenches become available. Proven assertions can be reused in system-level testbenches, for example, as coverage points or to speed integration verification.

The Integrated 360 MV Product Family

The 360 MV product family comprises five integrated products that cover the six application levels shown in Figure 1. Each step up in the product family extends previous products with new features and benefits, enabling additional application levels (see Figure 2).

360 MV Inspect™: Autochecks Step-by-step
360 MV Inspect allows designers to detect RTL errors as soon as first code is available. This enables an early, fast sanity check and code clean-up that reduces subsequent debugging effort. It exhaustively proves an extensive set of checks that the tool automatically extracts from the RTL code – verifying thousands of checks in minutes. These checks detect common design errors such as out-of-bound array access and stuck-at faults, identify design optimization opportunities such as dead code and constant registers, and detect synthesis/simulation mismatches. 360 MV Inspect requires no formal verification experience and no familiarity with assertion languages.

360 MV Check™: Verification of Implementation Intent
Using 360 MV Check, designers detect implementation bugs earlier and faster than using simulation, achieving earlier code bring-up quality and reducing subsequent debugging effort. Designers write simple white-box assertions to verify micro-architecture and implementation aspects of the RTL code. Typical use cases include integrity checks of data types, FSM states and transitions, verifying cause/effect relations between signals, and, e.g., correct error handling.

360 MV Verify™: Verification of Functional
Requirements and Design Operations debug
360 MV Verify provides the highest capacity and performance on the market to finds deep, complex errors much more efficiently than simulation, reducing the development effort for high coverage testbenches. Using 360 MV Verify, design and verification engineers write more complex assertions to verify functional requirements derived from the specification. Typical use cases are the verification of arbitration strategies, protocol compliance, and interrupt handling schemes. OneSpin's Timing Diagram Assertion Library – TiDAL – boosts productivity by easing the capture of functional requirements as SystemVerilog Assertions derived from waveforms and timing diagrams. 360 MV Verify provides most advanced debug automation capabilities for complex SVAs (see Figure 3) available in formal ABV tools today. It eliminates most of the time-consuming, error-prone manual analysis of complex information otherwise necessary to trace the root causes of assertion failures, speeding assertion and design debug by up to 10x.
Moreover, 360 MV Verify is the entry to OneSpin's unique, operation-based formal ABV. It guides users in the systematic verification of design operations, such as an 'AHB read' or the read/write operations of a cache controller. This operation-based approach – familiar to testbench developers – allows the user to formally verify the design's full functionality, achieving higher design confidence with significantly less effort than simulation. This approach eases assertion development by using TiDAL, working from waveforms and timing diagrams that describe the behavior of DUV operations and transactions. 360 MV Verify reduces or even eliminates the need for complex module/subsystem testbenches. The resulting verification quality significantly reduces time-consuming error-correction loops during integration-level and chip-level verification. Additional applications of this approach are systematic reverse engineering of IP and safe-guarded redesign of IP.

360 MV Assure™: Verification Employing Automatic Gap Detection
Users familiar with 360 MV Verify and its operation-based formal ABV approach can further increase verification quality by employing 360 MV Assure to automatically detects missing assertions in SVA property sets. Gap detection identifies yet unverified design behavior. A comprehensive debug and diagnosis environment guides the user in the development of additional assertions to close these verification gaps. Detected gaps often indicate errors and omissions in the specification and verification plan. So, 360 MV Assure enables a very thorough specification/implementation co-verification.

360 MV Certify™: Gap-Free Verification
360 MV Certify, the flagship of the 360 MV product family, achieves highest design confidence – as required, for example, for mission-critical IP – that cannot be ensured by any other verification approach currently available. 360 MV Certify implements OneSpin's GapFreeVerification™ process which guides users through all phases of verification planning, assertion development, and gap-detection checks to achieve gap-free formal verification of full design functionality. It guides the development of a gap-free set of SVA assertions to build a specification-compliant reference model of the full DUV functionality, and proves that the RTL code is functionally equivalent to this reference model.

Product Integration and Interoperability

All 360 MV products are integrated in the same verification environment featuring, among others, frontends for Verilog, SystemVerilog, and VHDL, powerful proof engines, programmable Tcl shell, design browsers, assertion development and debug/diagnosis environments, waveform and temporal fan-in viewer, fully-featured proof-status management including dependency tracking, and more. OneSpin also offers optional prover licenses for all products, as well as support for distributed execution in compute server networks.

Step-by-step Adoption and Use
360 MV's comprehensive spectrum of application levels and use cases enables users to choose the verification steps and products best suited to their formal verification experience, project schedule, available resources and required quality level (see Figure 2).
Users can then employ a mix of simulation and 360 MV to achieve the best effort/quality combination. Each 360 MV product improves the overall verification, and each introduces users to increasingly advanced formal verification concepts that enable higher verification productivity and quality. This step-by-step learning and adoption approach allows even formal verification newcomers to leverage the advantages of formal verification and become productive in a matter of days.