Synopsys 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.
What is Datapath Validation?
Synopsys VC Formal DPV is a formal verification tool that verifies the correct implementation of data path elements of a design. It uses formal algorithms to thoroughly prove the transactional equivalence between a golden specification in C/C++ and the RTL designs. While simulation is a useful verification tool, due to the size of the mathematical operations involved in modern designs, it is not possible to catch all design bugs. Formal verification is a must-have technology in every verification flow to find corner cases bugs and achieve formal sign-off.
As shown in the figure above, Synopsys VC Formal DPV supports many use cases – 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. Synopsys 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 Synopsys 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:
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 Synopsys 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 Synopsys VC Formal DPV.
Creative usages of Synopsys 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. Synopsys VC Formal DPV is a must-have tool for organizations in the verification flow.