²ÝÁñÉçÇø

²ÝÁñÉçÇø VC Formal Datapath Validation (DPV) is a technology that has long been deployed by top semiconductors companies and has enjoyed many success stories in CPU, GPU, and DSP designs. In recent years, as Artificial Intelligence (AI) and Machine Learning (ML) algorithms continue to advance, AI/ML chips become another key application domain for VC Formal DPV. In this blog, we will explain what datapath validation means and showcases a couple of customer use cases.

As shown in the figure above, ²ÝÁñÉçÇø VC Formal DPV supports many use cases ¨C C/C++ to C/C++ comparison, C/C++ to RTL comparison, and RTL to RTL comparison. VC Formal DPV has also been used as a theorem prover to verify complex multiplication functions. Since its inception (as HECTOR technology) 20 years ago, many creative usages of VC Formal DPV have been published. ²ÝÁñÉçÇø VC Formal DPV has been nicknamed ¡°Bug Vending Machine¡± because it has found many high-stake bugs in the customer designs.

NVIDIA VC Formal DPV Use Case

At the ²ÝÁñÉçÇø VC Formal Special Interest Group (SIG) 2022 event, Ashley Xiang, Formal Verification Engineer at NVIDIA, presented about using VC Formal DPV to verify their high-level synthesis (HLS) flow, starting from ensuring the C/C++ spec works properly by using VC Formal DPV to verify the embedded assertions; it then verifies that the HLS generated designs match the spec functionality. The following is the HLS verification flow NVIDIA presented using VC Formal DPV:

1. Evaluating the need and selecting designs that are computational heavy to deploy VC Formal DPV.
2. Using VC Formal DPV in an assertions-based verification (ABV) methodology to verify the embedded assertions in the C/C++ code for initial bug hunting and verification. This ensures the high-level spec is correct before synthesis.
3. Next, the traditional VC Formal DPV use model of verify C/C++ spec against RTL implementation is used to signoff of HLS generated RTL. This may involve optimizing the abstraction level of both designs and deploying intelligent convergence techniques to achieve full convergence and signoff.
4. Lastly, when there are incremental usages, VC Formal DPV can be used to verify two RTL implementations to ensure the changes have not introduced additional bugs.

The figure above shows the HLS flow presented by NVIDIA. VC Formal DPV is used to verify the C/C++ spec using ABV, as well as proving transactional equivalence of C/C++ to RTL, and RTL to RTL. NVIDIA has achieved great success using this workflow, finding many corner bugs, such as those related to calculation accuracy and illegal data range.

Intel VC Formal DPV Use Case

Intel and other leading companies are also utilizing advanced formal techniques like VC Formal DPV to verify their complex designs. In the session titled ¡°Formally Verifying Complex Algorithms¡±, Disha Puri, Formal Verification Engineer Manager at Intel, discussed deploying ²ÝÁñÉçÇø VC Formal DPV to verify compression blocks.

Compression is very difficult to verify using simulation and other techniques, because these designs often require data spaces that are massive, making traditional verification techniques ineffective. To overcome these challenges, Intel¡¯s engineers used various convergence solving techniques in VC Formal DPV, such as case splitting and assume guarantee techniques. They optimized the C++ specification to achieve the right level of abstraction for each chunk, and then proved an intermediate lemma for each, making it an assumption for the following blocks in the design. This resulted in significant improvements in convergence, with the most complex blocks converging in 20-30 hours, which could not be done in previous projects without the use of ²ÝÁñÉçÇø VC Formal DPV.

Conclusion

Creative usages of ²ÝÁñÉçÇø VC Formal DPV at NVIDIA and Intel are representative of the value of this tool when finding corner case bugs and achieving datapath signoff. It improves verification efficiency and increase the confidence of critical design quality. ²ÝÁñÉçÇø VC Formal DPV is a must-have tool for organizations in the verification flow.