你是否會(huì)遇到以下問題:bug可能比較微妙,不直觀,無法手動(dòng)推斷;或者在被觀察到之前就被激活很久了,傳統(tǒng)的模擬設(shè)計(jì)需要花很長(zhǎng)時(shí)間自動(dòng);驗(yàn)證工作量隨著設(shè)計(jì)復(fù)雜性的增加而增加,人工推理和手動(dòng)編寫屬性不再可行,等等。目前驗(yàn)證CPU的主流方法,如HW Testbench,
Universal Verification Methodology (UVM),
SW Testbench, Property Checking,
這些現(xiàn)有方法具有范圍受限、仿真較慢、long bug traces、需要手動(dòng)編寫test的特點(diǎn)。
那么,如何可靠、快速、自動(dòng)地驗(yàn)證處理器硬件,并且生成bug trace?
NO.1
形式化驗(yàn)證的開展基于形式化規(guī)范和自動(dòng)推理。其中形式化規(guī)范是指通過形式化語言將DUV和待證明的屬性建模成形式化模型,自動(dòng)推理是指通過嚴(yán)格的數(shù)學(xué)方法來推導(dǎo)DUV和待證明屬性規(guī)范之間的邏輯關(guān)系,通常是證明DUV的形式化模型能滿足所有形式化屬性規(guī)范。
形式化驗(yàn)證的基本步驟:
系統(tǒng)建模:把系統(tǒng)轉(zhuǎn)換為能被模型檢測(cè)工具所接受的形式。這是模型檢測(cè)的首要步驟,構(gòu)建系統(tǒng)模型時(shí)為了提高驗(yàn)證過程的效率及可行性需要將和要驗(yàn)證的屬性無關(guān)的細(xì)節(jié)抽象掉,僅保留與此相關(guān)的細(xì)節(jié),這是一個(gè)比較簡(jiǎn)單但通常會(huì)比較繁瑣的過程。
形式化規(guī)范:在對(duì)模型進(jìn)行驗(yàn)證之前以邏輯公式的形式給出待驗(yàn)證的屬性。命題時(shí)態(tài)邏輯能夠表達(dá)出系統(tǒng)的行為如何隨著時(shí)間而發(fā)生變化,因而通常被用來描述規(guī)范。一條規(guī)范只是描述了系統(tǒng)某一個(gè)屬性,一組規(guī)范是否覆蓋了系統(tǒng)需要滿足的所有屬性一直是個(gè)開放問題。規(guī)范開發(fā)的人力投入也是長(zhǎng)期困擾形式驗(yàn)證的問題。
形式化驗(yàn)證:模型檢測(cè)工具對(duì)輸入的模型的狀態(tài)空間進(jìn)行搜索來確定輸入的規(guī)范是否為真,為真表示模型滿足規(guī)范;為假則表示模型不滿足規(guī)范,此時(shí)會(huì)給出一個(gè)反例來說明規(guī)范為假的原因。
NO.2
QED(快速錯(cuò)誤檢測(cè))是一種識(shí)別錯(cuò)誤的方法(主要在處理器中,但也可用于其他組件),它將一組原始測(cè)試轉(zhuǎn)換為QED檢查。這涉及到將寄存器文件分成兩部分,其中一半用于原始指令,另一半用于重復(fù)的指令序列,原始序列和復(fù)制序列都以相同的順序執(zhí)行相同的指令,但它們是交錯(cuò)的,在原始指令序列和復(fù)制指令序列完成后,寄存器文件的兩部分應(yīng)該匹配。
根據(jù)經(jīng)驗(yàn),與傳統(tǒng)技術(shù)相比,這種方法可以將bug trace的長(zhǎng)度減少多達(dá)6個(gè)數(shù)量級(jí)。
Bounded Model Checking(BMC)用于驗(yàn)證有限狀態(tài)模型的正確性。它通過遍歷有限長(zhǎng)度的路徑來檢查模型是否滿足給定的性質(zhì)。
SQED基于BMC進(jìn)行符號(hào)運(yùn)算搜索所有指令序列組合。這為我們提供了一種無需編寫測(cè)試就可以驗(yàn)證處理器的方法,也不需要提供任何手寫屬性,只依賴于SQED檢查。是對(duì)傳統(tǒng)的形式驗(yàn)證方法的突破。
NO.3
基于SQED的指令集形式驗(yàn)證具有如下特點(diǎn)
全自動(dòng)驗(yàn)證:Symbolic Instructions + Self-Consistency Checking,不需要開發(fā)屬性集。
高覆蓋率:BMC工具搜索給定深度的所有指令序列。
最簡(jiǎn)bug復(fù)現(xiàn):BMC工具自動(dòng)生成從復(fù)位狀態(tài)到bug site的最短路徑。
借助AveMC高性能形式驗(yàn)證平臺(tái),AveMC/SQED組合為芯片設(shè)計(jì)指令集驗(yàn)證提供了全新的驗(yàn)證解決方案。
NO.4
AveMC在開源RISC-V上的SQED驗(yàn)證過程: 給定RISC-V核的RTL實(shí)現(xiàn)和ISA SPEC,從ISA SPEC中自動(dòng)解析生成QED Module(一個(gè)新的RTL),將原有的RISC-V核和QED Module連接起來。這里AveMC就可以直接進(jìn)行驗(yàn)證了。
指令集形式驗(yàn)證是芯片設(shè)計(jì)驗(yàn)證中的新興方向,在RISCV和AI/ML硬件加速芯片的驗(yàn)證中得到越來越廣泛的應(yīng)用。SQED是指令集形式驗(yàn)證領(lǐng)域的新興工具,它通過完全自測(cè)試的特性解決了驗(yàn)證屬性開發(fā)的低效和覆蓋率問題。在上海阿卡思微電子技術(shù)有限公司形式驗(yàn)證平臺(tái)AveMC上,SQED得到了成功的實(shí)現(xiàn)。與開源形式驗(yàn)證工具相比,AveMC/SQED不僅提升了驗(yàn)證速度,還能發(fā)現(xiàn)其他工具無法發(fā)現(xiàn)的bug。
上海阿卡思微電子技術(shù)有限公司由硅谷回國的資深電子設(shè)計(jì)自動(dòng)化(EDA)專家于2020年在上海張江高科技園區(qū)設(shè)立,旗下子公司成都奧卡思微電科技有限公司于2018年在成都高新區(qū)創(chuàng)立,公司聚集國際知名EDA公司和芯片設(shè)計(jì)公司具有多年研發(fā)經(jīng)驗(yàn)的尖端人才,基于形式化方法為邏輯芯片設(shè)計(jì)和工控軟件等提供驗(yàn)證工具及咨詢服務(wù),憑借在形式化方法領(lǐng)域深厚的技術(shù)積累及深入的產(chǎn)品實(shí)踐,公司已推出系列商用性能優(yōu)異的驗(yàn)證工具,服務(wù)于復(fù)雜芯片設(shè)計(jì)及通用設(shè)計(jì)流程,獲得多個(gè)標(biāo)桿客戶的采購使用。在研產(chǎn)品及應(yīng)用包括高階等價(jià)驗(yàn)證、功能安全等,覆蓋數(shù)字信息、智能硬件、航空航天、人工智能等行業(yè)需求。公司將最新的EDA技術(shù)與本土用戶需求相結(jié)合,服務(wù)于中國集成電路自主可控設(shè)計(jì);將產(chǎn)品開發(fā)與數(shù)字產(chǎn)業(yè)趨勢(shì)相結(jié)合,服務(wù)于中國技術(shù)創(chuàng)新與技術(shù)趕超;將技術(shù)推廣與產(chǎn)品優(yōu)化相結(jié)合,服務(wù)于海內(nèi)外需求市場(chǎng)。致力于成為國內(nèi)領(lǐng)先的形式化技術(shù)開發(fā)與服務(wù)商。
審核編輯:湯梓紅
-
cpu
+關(guān)注
關(guān)注
68文章
10721瀏覽量
209610 -
芯片設(shè)計(jì)
+關(guān)注
關(guān)注
15文章
982瀏覽量
54632 -
指令集
+關(guān)注
關(guān)注
0文章
221瀏覽量
23293 -
RISC-V
+關(guān)注
關(guān)注
44文章
2147瀏覽量
45739
原文標(biāo)題:基于AveMC/SQED的RISC-V指令集驗(yàn)證,芯片設(shè)計(jì)驗(yàn)證領(lǐng)域的一個(gè)新興方向
文章出處:【微信號(hào):gh_ca7d2d1f4371,微信公眾號(hào):阿卡思微電子】歡迎添加關(guān)注!文章轉(zhuǎn)載請(qǐng)注明出處。
發(fā)布評(píng)論請(qǐng)先 登錄
相關(guān)推薦
評(píng)論