Synopsys White Paper

Unlocking Formal Signoff Methodology

The last decade has seen a significant rise in the adoption of formal verification across the industry. This growth has led to a rapid diversification from user-defined Formal Property Verification (FPV) to the utilization of multiple applications to solve the most demanding verification and time to market (TTM) challenges. The emergence of formal verification as a mainstream tool has consequently sparked a persistent demand for a systematic formal verification signoff methodology. This methodology is crucial to both qualify and quantify the work performed.

There are various metrics that are crucial to the signoff process, serving to continually measure verification completion throughout the formal verification cycle. Engineers required a tool that could effectively bridge the correlation between formal verification effort and existing functional verification and code coverage metrics. In addition, formal verification engineers would often grapple with the same common questions during the formal signoff process:

• Have we written enough properties?
• Are constraints too strong?
• What is being verified?
• Can all bugs be caught?
• Can we map the data to functional coverage metrics?
• How do we merge all the metrics to a single database?
• How do we view the data in one place and analyze/debug it?

A robust and effective formal signoff methodology not only needs to provide answers to these questions, but also ensure ease of adoption and implementation in actual formal verification projects. Synopsys VC Formal™ leverages the latest formal technologies and AI/ML capabilities and supports the most rigorous formal signoff criteria. This whitepaper provides an overview of how VC Formal enhances and simplifies the formal signoff flow.