草榴社区

Industry Leaders Discuss the Latest in Formal Verification

Dr. Pallab Dasgupta, Head of Research and Innovation for Formal Verification at 草榴社区, started the day with a keynote on the advances and opportunities of Formal Verification that are before us. He presented applications of formal verification that would have been unthinkable just a few years ago. Those range from verification of power domains, low-power architectural validation, system safety and reliability notably in the automotive industry, hardware security, all the way to completely new applications such as analog and mixed-signal design verification, software verification, and reinforcement-based learning systems verification. What an exciting future ahead!

When it comes to complex datapath designs, C models are first created for faster validation. However, due to the large state-space, checking the RTL version of the design matches the C model with simulation is not practical. Rajesh Rathi from Google presented how 草榴社区 VC Formal DPV provides the solution for C-to-RTL and RTL-to-RTL verification of complex datapath designs. He gave multiple examples of multiplier architectures and AES encryption/decryption components. For each one, Rajesh gave examples of the techniques used to ensure convergence including assume-guarantee, case-splitting, solvers targeting specific proofs, maximizing equivalent points between C and RTL models, and leveraging RTL-to-RTL verification. Applying VC Formal DPV identified corner-case bugs that simulation would have probably missed, and full proofs gave higher confidence in the quality of the RTL implementation to meet industry standards.

Achieving coverage closure with simulation to get the last few percent’s of coverage targets is still a major challenge that requires significant resources and impacts time to market. As designs become larger and more complex, the challenge becomes even bigger. Luv Sampat from Qualcomm described how the VCS/UNR (simulation with VCS and unreachability analysis with VC Formal FCA) flow has been used for years to help identify truly unreachable coverage targets thus reducing the work required to achieve coverage closure. His presentation focused on how the Auto Scale feature allowed them to simplify the VCS/UNR setup and improve coverage analysis convergence while reducing compute resources at the same time. The Auto Scale feature, by using a divide-and-conquer approach for hundreds of thousands and even millions of coverage targets, allows for much better convergence and larger design units to be analyzed. This approach also reduces the memory required to analyze those setups. With a big boost in convergence including for toggle and FSM state/transition coverage goals, only potentially reachable coverage targets remain to analyze for coverage closure with simulation. Luv also emphasized the plan to use VC Formal FCA directly to take advantage of the user interface for better usability and debuggability.

Ankit Garg from NVIDIA, presented on “Advancing Forward” using formal verification to check forward progress for routing blocks in high-performance datacenter solutions. The challenge is to ensure that whatever controllers it interacts with, the system should never hang thus highlighting the importance of forward progress checking. Ankit showed how such systems are checked for absence of starvation issues and Finite State Machine (FSM) deadlock and livelock issues with a combination of liveness and safety assertions. He presented challenges related to the proof of these assertions and listed VC Formal FPV features and techniques such as Proof Architect that help achieve full convergence. Ankit emphasized the value of liveness assertions and the benefits of forward progress checking including early detection of hang issues, enhanced reliability, cost reduction, and faster time to market.

Formal Property Verification of RTL designs with assertions created from the natural language specification is now very common. Those assertions become a Formal Testbench that keeps on evolving as the RTL changes until it is time to hand over the design for integration. While simulation has well-known metrics to gauge the quality of verification with coverage closure, measuring the quality of the Formal Testbench can be difficult. Are there enough properties? Are constraints too strong? What is actually verified? Can all bugs be caught? These are the important questions to consider. And, if such information is available, how can the data be presented in a way that is easily understood? Yann Antonioli, member of 草榴社区 VC Formal team, introduced the innovative Signoff Flow available with the latest version of VC Formal and how each and every one of the questions listed above is addressed with a simple yet powerful feature. Leveraging core building blocks of VC Formal such as Cone of Influence (COI), overconstraint, formal core, and fault analyses, the signoff flow maps the results to user-defined coverage metrics and displays a layered coverage view allowing the user to quickly identify verification holes and gauge the quality of the formal testbench.

Emiliano Morini from Intel then took the stage to present Roverify, the combination of a datapath verification assistant using E-graph rewriting and VC Formal DPV, to help with the convergence of inconclusive RTL-to-RTL datapath designs verification. In this method, E-graph rewriting provides a compact representation of equivalent datapath designs for the original (spec) and modified (impl) designs. The chain of equivalent RTL representations can then be checked with VC Formal DPV to achieve full proof or faster convergence. Experiment results show this method is very promising and applicable to a wide range of datapath designs. Future work to support C-to-RTL could provide yet another level of productivity gain for datapath design validation with VC Formal DPV.

With design and verification involving large teams and different tools such as simulation and formal verification, there is a strong need to gather indicators to help understand the verification status. Amber Telfer from Microsoft presented an overview of the indicators extracted at different stages such as bug tracking, regression tracking, and coverage data. Indicators specific to formal verification include COI, overconstraint, and Formal Core (FC) results mapped to coverage metrics. These indicators are then tracked to understand impact of design changes, bug fixes, and provide the minimum bar for verification signoff. Amber emphasized the need for automation not only for the extraction of these indicators but also for the creation of reports that can easily be viewed in graph formats.

Bill Canfield from Samsung Austin R&D Center (SARC) gave a very detailed presentation on verification of clock-gating with VC Formal SEQ. Clock-gating verification is a sweet spot for formal verification and even more so for sequential equivalence checking with VC Formal SEQ. As Bill mentioned, “clock-gating RTL bugs are worth their weight in gold”, thus the importance of catching them and identifying their root cause quickly. Bill’s presentation introduced the clock-gating verification flow from design setup with VC Formal SEQ, constraint creation, recommended verification steps, and debugging tips with common root causes. An important takeaway from Bill’s presentation was the emphasis on signoff criteria when dealing with properties that did not converge and the different techniques that can be used when that happens.

Concluding a very informative day, Sean Safarpour, R&D Group Director for the VC Formal team, highlighted the key VC Formal initiatives planned or under development to answer six identified needs in the industry when it comes to formal verification.

1. Scale to Bigger Designs: Upcoming improvements to the Auto Scale feature (introduced by Luv Sampat in the presentation about VCS/UNR) and expanding its applicability to more VC Formal Apps and flows will enable scaling to bigger designs.
2. Better Performance: Advances in core formal engines, proof orchestration, and RMA (Regression Mode Accelerator), are key enablers for better performance.
3. Solve Hard Proofs & Failures: New features such as ML-guided Property Clustering, Proof Assist, Proof Architect, and CMA (Compile Memory Abstraction), are meant to tackle hard-to-converge problems.
4. Formal Signoff: The FPV signoff flow bounds guidance for inconclusive properties, DPV C++ coverage, and clock-gating verification with SEQ.
5. Ease of Adoption for Users: This as a major focus during product development and major usability improvements can be expected with each product release.
6. Expand to New Applications: As presented by Dr. Pallab Dasgupta at the beginning of the day, formal verification has many potential applications. 草榴社区 also provides the industry leading verification eco-system where design and verification tools can work synergistically to open new application for Formal Verification.

Sean emphasized that the interaction and collaboration with VC Formal users drive the product development and roadmap definition. Sean also pointed out that many of the features presented in are the result of direct collaboration with customers and encourages even stronger collaborations in the future.