OneSpin 360 MV™ Module Verifier
The Only Gap-Free Formal SVA Verification Solution
Highlights
- Automated verification gap detection ensures highest possible design and verification quality
- Intuitive, SVA-based verification of module-level operations eases and speeds learning and use
- GapFreeVerification™ process guides verification planning, execution, debug and formal coverage analysis
- Closed-loop verification process slashes effort by up to 5X compared to 'thorough' testbenches
- Highest capacity and performance formal SVA verification solution handles designs with several 100K lines of RTL code flat
Now You Can Perform Efficient Gap-Free Verification using SVA
The OneSpin 360™ Module Verifier (360 MV) delivers the industry's first GapFreeVerification™ process,
the only closed-loop process that guides and fully integrates verification planning, execution,
debug and formal coverage analysis for digital modules and intellectual property (IP).
The solution's patented verification gap detection automatically identifies unverified functionality
as well as specification errors and omissions, and provides comprehensive ongoing visibility of verification status.360 MV's technology is the first to integrate verification planning, execution and verification quality analysis into a closed-loop process – the key to significantly higher productivity and highest verification quality. The verification plan drives property development, and properties are proven against the RTL code. Unlike other formal verification approaches, 360 MV automatically detects gaps in the property set (see figure 1). The identification of incomplete properties drives improvement of individual properties, while the identification of missing properties drives completion of the verification plan and the property set. This systematic, incremental application of gap detection greatly simplifies verification planning and property development by eliminating the need to anticipate potentially erroneous behaviour and corner-case scenarios in the design-under-verification (DUV).
Know When Verification is Done
The closed-loop process iterates until all properties hold on the DUV and automatic gap detection confirms that the property set contains no further gaps. At this point, the property set is known to be a golden reference model for the full intended functionality of the DUV, and the DUV's actual functionality is confirmed to be equivalent to the reference model. Gap-free verification has been achieved, so verification can then be terminated with confidence. GapFreeVerification thus replaces the verification closure 'confidence guessing game' common with testbenches and other formal approaches.Achieve the Highest Possible Quality
The closed-loop process achieves the highest possible verification and design quality essential to risk-free design use and reuse. Automated gap-detection, integrated with property development and verification, automatically identifies gaps in the property set. For example, the user may have forgotten to describe the intended value of some output signal in a specific situation, or to describe an execution mode of an operation. Besides quickly identifying necessary improvements to the property set, this analysis typically finds as many errors and omissions in the informal specification as in the RTL code of the DUV. It is thus a true specification/implementation co-verification solution.Automatic gap detection closes the process loop of GapFreeVerification and replaces tedious and error-prone manual reviews and coverage approaches with a faster, reliable, fully automatic solution.
Easily Capture Module-Level Properties in SVA
The 360 MV solution leverages an intuitive verification methodology using the SystemVerilog Assertion (SVA)
language to capture module-level operations as properties, which eases and speeds learning and use.
The operation properties directly capture specification intent, utilizing OneSpin's ground-breaking
SVA-based TIming Diagram Assertion Library, TIDAL™.
TIDAL enables easy development of properties from familiar operation timing diagrams, greatly reducing the complexity
of SVA-based verification and enabling new users to become productive in two weeks.In addition, 360 MV offers the most comprehensive formal SVA verification solution, supporting fully automatic RTL code checks, implementation verification using low-level SystemVerilog assertions, and verification of high-level requirements written in SVA. 360 MV then extends this solution range with its unique gap-free verification process employing SVA
(see figure 2).
Substantially Boost Productivity
The 360 MV solution slashes verification effort by up to 5X compared to 'thorough' testbenches (see figure 3). Its automated gap detection greatly simplifies and speeds verification planning by eliminating the time and effort to anticipate potentially erroneous DUV behaviour, as well as corner cases. 360 MV reduces verification time and effort by eliminating the need for coverage models, coverage data collection, and coverage data analysis. Its gap-free verification of modules prior to integration and system-level verification mitigates or even eliminates error-correction loops to address module-level bugs uncovered during system-level verification.
Simplify IP Lifecycle Management
In addition to highest verification quality, OneSpin's GapFreeVerification process enables an IP provider to provide IP users with a specification that comprehensively and accurately describes the IP's behavior under precisely-defined integration conditions, allowing rapid adaptation and correct integration, substantially reducing or even eliminating the typical IP 'time-to-maturity phase' of 6 to 24 months.Verify Beyond The Limitations of Common Formal Verification Tools
360 MV is the industry's highest capacity formal solution, enabling verification of designs in excess of 100K lines of RTL code flat – an order of magnitude greater than other formal tools. The operation-based verification methodology, combined with advanced proof engines, enables the verification of properties beyond 10K state bits in their cone-of-influence without the need for abstractions and without suffering the state space explosion common in other formal tools. Also unlike other formal solutions, 360 MV can handle many of the arithmetic operators common in DSPs and other designs.Production-Proven on Hundreds of Designs
The 360 MV solution has been customer-proven on hundreds of complex modules and IP designs such as processors, digital peripherals, memory controllers, bus bridges, and subsystems of up to a few hundred thousand lines of RTL code.read more about: