新思科技VC Formal DPV可對任何數(shù)據(jù)路徑塊進行簽核

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

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

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

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

過去20年間，新思科技不斷升級形式求解器，性能越來越完善，促使許多客戶開始使用HECTOR來驗證CPU、GPU、網(wǎng)絡(luò)和安全性應用中的ALU、FPU和DSP塊。2017中，HECTOR技術(shù)被整合到新思科技 VC Formal? Datapath Validation （DPV） App中，該應用現(xiàn)已能夠支持所有現(xiàn)代C++語言和基于業(yè)界領(lǐng)先的新思科技 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ù)設(shè)計改進，而無需任何驗證平臺、斷言或覆蓋率要求。VC Formal DPV可以靈敏地檢測極端缺陷，從而避免代價高昂的錯誤發(fā)生。該技術(shù)嵌入了：

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

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

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

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

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

隨著電子設(shè)備變得越來越智能，人工智能（AI）和機器學習（ML）芯片被廣泛應用于許多領(lǐng)域。由于AI/ML芯片使用浮點運算來處理大量數(shù)據(jù)，因此VC Formal DPV非常適合此類芯片設(shè)計，獲得了全球AI/ML初創(chuàng)企業(yè)的大量部署。

為了幫助企業(yè)采用數(shù)據(jù)路徑驗證方法，新思科技提供了經(jīng)過形式驗證的全面的C++數(shù)學庫來驗證RTL，并且還為交鑰匙項目的培訓和執(zhí)行提供咨詢服務。

數(shù)據(jù)路徑驗證的前景十分光明。新思科技憑借20多年的HECTOR技術(shù)投入和不斷革新，其VC Formal DPV可對任何數(shù)據(jù)路徑塊進行簽核。