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.