Automatic detection of verification gaps, specification omissions and errors
SystemVerilog Assertions and Operational SVA are very powerful in capturing functional requirements and verifying entire circuit operations. OneSpin Quantify™ provides intuitive coverage metrics, helping engineers spot verification gaps even in the presence of bounded proof results. OneSpin’s automatic integration with third-party verification planning tools ensures that all foreseen functional coverage points and checks are implemented and pass. This allows the user to efficiently achieve formal functional sign-off and provides a high confidence level. However, subtle bugs and skillfully crafted malicious issues in both design and specification could still go unnoticed.
OneSpin 360 DV-Certify™ automates the analysis of sets of Operational SVA, detecting inconsistencies, errors, and gaps in both verification plans and specifications. An intuitive debug environment enables engineers to pinpoint shortcomings and guides them on how to systematically improve their sets of assertions.
OneSpin 360 DV-Certify performs an automated formal analysis of sets of Operational SVA, capturing functional requirements and timing diagrams. This analysis does not depend on the actual RTL implementation. The user only needs to specify the set of RTL inputs and outputs of the functions under verification, the names of architecturally visible registers, and the names of the assertions to analyze. This information, referred to as Completeness Plan, is conveniently expressed in a separate file using SystemVerilog syntax. OneSpin 360 DV-Certify reveals inconsistencies and gaps, including fully- or partly-unverified interfaces, input transactions, or configuration scenarios omitted in the specification or overlooked during the verification planning phase. DV-Certify is based on unique, patented formal technology, and will either prove that the set of Operational SVA precisely matches the completeness plan, or point to scenarios that need further examination.
OneSpin 360 DV-Certify performs a comprehensive number of targeted formal checks. When a check fails, relevant debug information is produced that helps to quickly pinpoint the gap in the specification or verification plan. The debug environment is based on familiar simulation traces showing scenarios that have not been accounted for, and on annotated assertion view highlighting overlapping assertions addressing the same functionality. A crucial aspect of 360 DV-Certify is that it can be used during assertion development, and not just as a final sign-off check. As functional requirements are captured in Operational SVA, relevant sub-checks can be executed and debugged to detect any issues as early as possible.
Rigorous and Efficient Requirements Verification
OneSpin 360 DV-Certify supports the patented GapFreeVerification™ methodology, enabling the most rigorous and efficient functional verification process. Following this methodology, transaction-level requirements are captured in an ordered and phased manner. Specific subsets of 360 DV-Certify sub-checks are run at each development step, allowing engineers to detect and resolve issues early, before moving to subsequent phases.
OneSpin 360 DV-Certify and the GapFreeVerification™ methodology have track records of successful adoption in both large and small organizations focusing on safety-critical applications. A number of industrial case studies, including "The Complete Formal Verification of a Family of Automotive DSPs” from Bosch, are available online.