新思科技 VC Formal DPV是CPU、GPU和AI/ML設計數(shù)據(jù)路徑驗證的不二之選

我們生活在大數(shù)據(jù)的世界中：B站日均播放量17億次，微信每天發(fā)送約500億條信息。預計到2025年，全球每天生成的數(shù)據(jù)量有望達到463EB。

如此龐大的數(shù)據(jù)量，需要采用浮點算術運算的芯片才能夠以最快的速度和最高的精度進行處理、存儲、分析和共享。而驗證這些芯片上的數(shù)據(jù)處理邏輯（數(shù)據(jù)路徑）的正確性至關重要。歷史證明，未能及時發(fā)現(xiàn)錯誤將會導致高昂的代價。

鑒于此，新思科技很早就開始研究驗證復雜數(shù)據(jù)路徑邏輯的方法。例如，基于仿真的傳統(tǒng)驗證方法效率低、耗時長，而且對于無遺漏地驗證這些復雜的數(shù)學函數(shù)根本不切實際。以一個兩個32位操作數(shù)的簡單數(shù)學運算為例子，其中就會包含264個操作數(shù)對。假設處理速度為每秒30億次模擬速度，則需要195個計算年。這導致計算資源根本無法得到充分和高效利用。

形式驗證使用數(shù)學方法來證明或反駁預期算法的正確性，可提供一種有效、高效且可追溯的解決方案。在對函數(shù)正確性至關重要的復雜控制和數(shù)據(jù)路徑邏輯進行驗證時，它可對仿真方法起到補充作用。認識到設計架構師趨向于將規(guī)范編寫為C或C++參考模型，新思科技的研究團隊開始致力于開發(fā)一種驗證技術來確定硬件設計人員創(chuàng)建的RTL是否等效于C/C++模型。復雜數(shù)據(jù)路徑專用驗證解決方案HECTOR（High-level Equivalence C++ to RTL）由此誕生。

過去20年間，新思科技不斷升級形式求解器，性能越來越完善，促使許多客戶開始使用HECTOR來驗證CPU、GPU、網(wǎng)絡和安全性應用中的ALU、FPU和DSP塊。

2017中，HECTOR技術被整合到新思科技 VC Formal Datapath Validation (DPV) App中，該應用現(xiàn)已能夠支持所有現(xiàn)代C++語言和基于業(yè)界領先的新思科技 Verdi SoC Debug Platform的完整調(diào)試環(huán)境。

VC Formal DPV成為業(yè)界首個用于對數(shù)據(jù)路徑元素進行無遺漏驗證的商用形式驗證工具。 VC Formal DPV針對獨立開發(fā)的模型提供等效性檢查，無遺漏地驗證RTL實現(xiàn)是否與可信的C/C++參考模型等效，并且可用于無遺漏地驗證C到C、C到RTL，以及RTL到RTL等連續(xù)設計改進，而無需任何驗證平臺、斷言或覆蓋率要求。VC Formal DPV可以靈敏地檢測極端缺陷，從而避免代價高昂的錯誤發(fā)生。該技術嵌入了：

快速高效的形式算法，包括加入多個求解器用于解算復雜的數(shù)學邏輯

快速收斂技術，包括自動設計分區(qū)和多處理器支持

高級調(diào)試支持，包括一個集成的調(diào)試器，支持單步調(diào)試C/C++代碼

靈活的語言支持：Verilog、VHDL、SystemVerilog、C、C++

VC Formal DPV可提供100%的信任度，其RTL設計實現(xiàn)符合C/C++參考算法，因此與基于仿真的技術相比，可以顯著加快數(shù)據(jù)路徑組件的簽核。

隨著電子設備變得越來越智能，人工智能（AI）和機器學習（ML）芯片被廣泛應用于許多領域。由于AI/ML芯片使用浮點運算來處理大量數(shù)據(jù)，因此VC Formal DPV非常適合此類芯片設計，獲得了全球AI/ML初創(chuàng)企業(yè)的大量部署。 為了幫助企業(yè)采用數(shù)據(jù)路徑驗證方法，新思科技提供了經(jīng)過形式驗證的全面的C++數(shù)學庫來驗證RTL，并且還為交鑰匙項目的培訓和執(zhí)行提供咨詢服務。 數(shù)據(jù)路徑驗證的前景十分光明。新思科技憑借20多年的HECTOR技術投入和不斷革新，其VC Formal DPV可對任何數(shù)據(jù)路徑塊進行簽核。