Synopsys Cloud
Cloud native EDA tools & pre-optimized hardware platforms
Request a Free Trial →
Simulation and formal verification are two key verification strategies used in today¡¯s SoC design and verification flow. With their unique strengths and weaknesses, simulation and formal verification complement each other in finding corner case bugs and ultimately achieving verification closure and signoff.
Simulation and formal verification are usually done by different design verification and formal teams with their own set of signoff goals. These teams typically do not collaborate closely because formal verification and simulation can require different expertise and skillsets. However, there are synergies between simulation and formal that can greatly benefit the overall verification effort and accelerate coverage closure. In this blog, we will examine some of the technology connections between simulation and formal so that verification and formal teams can work together to incorporate both technologies effectively and efficiently to achieve verification signoff.
Why Achieving Coverage Closure is Challenging
Achieving coverage closure using simulation alone can be challenging. The time spent in simulation and the number of tests run don¡¯t correlate linearly with the percentage increase in coverage goals accomplished. As shown below, the coverage curve flattens despite increased simulation runs over time. This is usually due to two factors: 1) those coverage goals that are inherently unreachable; 2) those hard-to-hit coverage goals might require manual test creation as constrained random simulation may not hit those coverage targets. At some point, running countless simulation tests doesn¡¯t generate the best ROI nor lead to coverage closure.
How Formal Verification Can Accelerate Coverage Closure
Formal verification can address both challenges to accelerate simulation coverage closure in two ways:
- A Synopsys VC Formal app targeted specifically to analyze the reachability of those uncovered points, Formal Coverage Analyzer (FCA), can conclusively report whether those coverage goals are reachable. This analysis is often referred to as UNR (unreachability). If a coverage goal is not reachable, it could lead to two actions¨Cif the designers review and confirm this is expected, then those coverage goals can be removed from the verification plan so as to increase the coverage percentage reached. If this is not expected, then it is typically a design bug or an over-constrained environment that render user action to either fix the design bug or relax the design environment.
- Another way formal verification can help is through cover properties. Unlike verifying an assertion using formal technology where the tool will exhaustively prove the correctness of the property or produce a counterexample, the goal for cover properties is for the formal tools to produce a trace that shows how this cover point can be reached. Such a trace can aid in creating new simulation tests to hit those hard-to-cover coverage goals.
Benefits of Tight Integration Between Synopsys VCS and Synopsys VC Formal Verification 91³Ô¹ÏÍø
While the synergy between simulation and formal does not rely on both technologies coming from the same electronic design automation (EDA) vendor, there are additional benefits when both solutions share other technology commonality. The industry-standard Synopsys VCS simulator and our innovative Synopsys VC Formal solution share many other valuable connections benefiting end users.
- Synopsys VCS and Synopsys VC Formal solutions share a common compilation frontend. The unified compilation ensures easy adoption of VC Formal into VCS verification environments and consistent interpretation of design semantic and intent.
- The Synopsys VC Formal FCA app can be natively invoked within the VCS shell to do reachability analysis so as to identify unreachability goals, creating an unreachability exclusion file to be fed back to the VCS environment, improving simulation coverage.
- Cover properties run in the Synopsys VC Formal FPV app can help create additional simulation tests to cover the hard-to-hit points via random simulation.
- Also important is that with Synopsys VCS and VC Formal, simulation and formal coverage databases can be merged so that design elements verified with one technology may not need to be verified by another. This also greatly accelerates verification closure and signoff.
Substantial Savings in SoC Verification Effort
Many Synopsys VCS and VC Formal customers are seeing 40% to 80% savings in verification effort while gaining more confidence in achieving verification signoff. This table shows 10 customer designs and the impact of formal analysis in saving verification effort.
For support in maximizing the benefits of formal technologies, the Synopsys Formal Verification Services team provides experts around the world who can assist with methodology training, verification audit, and a variety of turnkey projects.
Summary
With their exhaustive capabilities, formal techniques can go a long way in helping prove chip design correctness. By enhancing your simulation methodology with formal technologies, you can accelerate coverage closure to achieve higher quality designs. The tight integration between the Synopsys VC Formal, Synopsys Verdi, and Synopsys VCS functional verification solutions delivers the speed, capacity, and flexibility to verify today¡¯s complex SoCs and get to the bottom of root causes of design bugs. Better yet, you won¡¯t have to be a formal expert to be productive with these solutions.
Synopsys silicon design and verification solutions share common technologies and consistent design interpretation that provide verification engineers with a seamless user experience, higher performance, and increased productivity. Continued innovation in ¡°value links¡± across Synopsys products enables companies to efficiently design the next wave of transformative products.
Stay tuned for future blog posts exploring how the connections between Synopsys VC Formal and the other tools in our verification toolbox facilitate fast, high-quality formal signoff.