我們生活在大數(shù)據(jù)的世界中:B站日均播放量17億次,微信每天發(fā)送約500億條信息。預(yù)計(jì)到2025年,全球每天生成的數(shù)據(jù)量有望達(dá)到463EB。
如此龐大的數(shù)據(jù)量,需要采用浮點(diǎn)算術(shù)運(yùn)算的芯片才能夠以最快的速度和最高的精度進(jìn)行處理、存儲(chǔ)、分析和共享。而驗(yàn)證這些芯片上的數(shù)據(jù)處理邏輯(數(shù)據(jù)路徑)的正確性至關(guān)重要。歷史證明,未能及時(shí)發(fā)現(xiàn)錯(cuò)誤將會(huì)導(dǎo)致高昂的代價(jià)。
鑒于此,新思科技很早就開始研究驗(yàn)證復(fù)雜數(shù)據(jù)路徑邏輯的方法。例如,基于仿真的傳統(tǒng)驗(yàn)證方法效率低、耗時(shí)長(zhǎng),而且對(duì)于無(wú)遺漏地驗(yàn)證這些復(fù)雜的數(shù)學(xué)函數(shù)根本不切實(shí)際。以一個(gè)兩個(gè)32位操作數(shù)的簡(jiǎn)單數(shù)學(xué)運(yùn)算為例子,其中就會(huì)包含264個(gè)操作數(shù)對(duì)。假設(shè)處理速度為每秒30億次模擬速度,則需要195個(gè)計(jì)算年。這導(dǎo)致計(jì)算資源根本無(wú)法得到充分和高效利用。
形式驗(yàn)證使用數(shù)學(xué)方法來(lái)證明或反駁預(yù)期算法的正確性,可提供一種有效、高效且可追溯的解決方案。在對(duì)函數(shù)正確性至關(guān)重要的復(fù)雜控制和數(shù)據(jù)路徑邏輯進(jìn)行驗(yàn)證時(shí),它可對(duì)仿真方法起到補(bǔ)充作用。認(rèn)識(shí)到設(shè)計(jì)架構(gòu)師趨向于將規(guī)范編寫為C或C++參考模型,新思科技的研究團(tuán)隊(duì)開始致力于開發(fā)一種驗(yàn)證技術(shù)來(lái)確定硬件設(shè)計(jì)人員創(chuàng)建的RTL是否等效于C/C++模型。復(fù)雜數(shù)據(jù)路徑專用驗(yàn)證解決方案HECTOR(High-level Equivalence C++ to RTL)由此誕生。
過(guò)去20年間,新思科技不斷升級(jí)形式求解器,性能越來(lái)越完善,促使許多客戶開始使用HECTOR來(lái)驗(yàn)證CPU、GPU、網(wǎng)絡(luò)和安全性應(yīng)用中的ALU、FPU和DSP塊。2017中,HECTOR技術(shù)被整合到新思科技 VC Formal? Datapath Validation (DPV) App中,該應(yīng)用現(xiàn)已能夠支持所有現(xiàn)代C++語(yǔ)言和基于業(yè)界領(lǐng)先的新思科技 Verdi? SoC Debug Platform的完整調(diào)試環(huán)境。VC Formal DPV成為業(yè)界首個(gè)用于對(duì)數(shù)據(jù)路徑元素進(jìn)行無(wú)遺漏驗(yàn)證的商用形式驗(yàn)證工具。
VC Formal DPV針對(duì)獨(dú)立開發(fā)的模型提供等效性檢查,無(wú)遺漏地驗(yàn)證RTL實(shí)現(xiàn)是否與可信的C/C++參考模型等效,并且可用于無(wú)遺漏地驗(yàn)證C到C、C到RTL,以及RTL到RTL等連續(xù)設(shè)計(jì)改進(jìn),而無(wú)需任何驗(yàn)證平臺(tái)、斷言或覆蓋率要求。VC Formal DPV可以靈敏地檢測(cè)極端缺陷,從而避免代價(jià)高昂的錯(cuò)誤發(fā)生。該技術(shù)嵌入了:
快速高效的形式算法,包括加入多個(gè)求解器用于解算復(fù)雜的數(shù)學(xué)邏輯
快速收斂技術(shù),包括自動(dòng)設(shè)計(jì)分區(qū)和多處理器支持
高級(jí)調(diào)試支持,包括一個(gè)集成的調(diào)試器,支持單步調(diào)試C/C++代碼
靈活的語(yǔ)言支持:Verilog、VHDL、SystemVerilog、C、C++
VC Formal DPV可提供100%的信任度,其RTL設(shè)計(jì)實(shí)現(xiàn)符合C/C++參考算法,因此與基于仿真的技術(shù)相比,可以顯著加快數(shù)據(jù)路徑組件的簽核。
隨著電子設(shè)備變得越來(lái)越智能,人工智能(AI)和機(jī)器學(xué)習(xí)(ML)芯片被廣泛應(yīng)用于許多領(lǐng)域。由于AI/ML芯片使用浮點(diǎn)運(yùn)算來(lái)處理大量數(shù)據(jù),因此VC Formal DPV非常適合此類芯片設(shè)計(jì),獲得了全球AI/ML初創(chuàng)企業(yè)的大量部署。
為了幫助企業(yè)采用數(shù)據(jù)路徑驗(yàn)證方法,新思科技提供了經(jīng)過(guò)形式驗(yàn)證的全面的C++數(shù)學(xué)庫(kù)來(lái)驗(yàn)證RTL,并且還為交鑰匙項(xiàng)目的培訓(xùn)和執(zhí)行提供咨詢服務(wù)。
數(shù)據(jù)路徑驗(yàn)證的前景十分光明。新思科技憑借20多年的HECTOR技術(shù)投入和不斷革新,其VC Formal DPV可對(duì)任何數(shù)據(jù)路徑塊進(jìn)行簽核。
-
人工智能
+關(guān)注
關(guān)注
1791文章
47229瀏覽量
238336 -
新思科技
+關(guān)注
關(guān)注
5文章
796瀏覽量
50335 -
數(shù)據(jù)路徑
+關(guān)注
關(guān)注
0文章
4瀏覽量
6302
發(fā)布評(píng)論請(qǐng)先 登錄
相關(guān)推薦
評(píng)論