基于時(shí)序邏輯等效性檢查方法的RTL驗(yàn)證

寄存器傳輸級(jí)(RTL)驗(yàn)證在數(shù)字硬件設(shè)計(jì)中仍是瓶頸。行業(yè)調(diào)研顯示，功能驗(yàn)證占整個(gè)設(shè)計(jì)工作的70%。但即使把重點(diǎn)放在驗(yàn)證上面，仍有超過(guò)60%的設(shè)計(jì)出帶需要返工。其主要原因是在功能驗(yàn)證過(guò)程中暴露出來(lái)的邏輯或功能瑕疵和缺陷等。顯然，需要進(jìn)一步改進(jìn)驗(yàn)證技術(shù)。

設(shè)計(jì)團(tuán)隊(duì)一般采用系統(tǒng)模型進(jìn)行驗(yàn)證。就驗(yàn)證來(lái)說(shuō)，系統(tǒng)模型比RTL更具優(yōu)勢(shì)，比如系統(tǒng)模型易于開(kāi)發(fā)且具有優(yōu)異的運(yùn)行時(shí)性能。挑戰(zhàn)性在于如何在系統(tǒng)級(jí)驗(yàn)證和生成功能正確的RTL間建立起橋梁。一種稱為時(shí)序邏輯等效性檢查的方法具有橋接兩者的能力，它是基于C/C++或SystemC編寫(xiě)的規(guī)范來(lái)對(duì)RTL實(shí)現(xiàn)進(jìn)行形式驗(yàn)證。

本文將討論商用圖形處理芯片所采用的從系統(tǒng)級(jí)到RTL的設(shè)計(jì)和驗(yàn)證流程。在該流程中，先要開(kāi)發(fā)出系統(tǒng)模型，然后用它來(lái)確認(rèn)視頻指令的算術(shù)運(yùn)算，然后再采用時(shí)序邏輯等效性檢查方法驗(yàn)證RTL實(shí)現(xiàn)。

系統(tǒng)級(jí)流程

隨著設(shè)計(jì)復(fù)雜性的增加，為了仿真整個(gè)系統(tǒng)，系統(tǒng)級(jí)建模變得不可避免。伴隨功能劃分、模塊接口和硬件/軟件協(xié)同設(shè)計(jì)而來(lái)的設(shè)計(jì)復(fù)雜性呈指數(shù)形式增長(zhǎng)，使得系統(tǒng)驗(yàn)證勢(shì)在必行。目前常采用C/C++或SystemC進(jìn)行系統(tǒng)級(jí)設(shè)計(jì)和驗(yàn)證。

本例采用了C/C++來(lái)建模視頻處理算法模塊。一旦系統(tǒng)模型完成了調(diào)整和驗(yàn)證，RTL設(shè)計(jì)師就可以編寫(xiě)Verilog代碼。高層綜合工具可以從系統(tǒng)代碼生成RTL。但工程師更常見(jiàn)的做法是用RTL代碼手工重新編寫(xiě)設(shè)計(jì)。它是設(shè)計(jì)的解釋而非轉(zhuǎn)換。即便已用多種驗(yàn)證測(cè)試平臺(tái)對(duì)RTL實(shí)現(xiàn)進(jìn)行了驗(yàn)證，采用基于仿真的方法也無(wú)法測(cè)試全部可能的狀態(tài)。

在設(shè)計(jì)流程中有許多驗(yàn)證工具和方法可以采用，它們包括：基于斷言的驗(yàn)證，隨機(jī)激勵(lì)生成和以覆蓋率驅(qū)動(dòng)的驗(yàn)證等。上述方法在功能上也許是值得依賴的，但它們都沒(méi)有借助系統(tǒng)模型。時(shí)序邏輯等效性檢查方法可以將系統(tǒng)模型的這種信心直接轉(zhuǎn)換為RTL實(shí)現(xiàn)。

圖形處理器市場(chǎng)受成像質(zhì)量、再現(xiàn)性能和用戶購(gòu)買時(shí)機(jī)的影響很大。對(duì)負(fù)責(zé)研制最新圖形處理器芯片的項(xiàng)目團(tuán)隊(duì)來(lái)說(shuō)，上述因素要求他們迅速開(kāi)發(fā)出新算法、拿出新設(shè)計(jì)。為了滿足這種要求，可以采用系統(tǒng)模型來(lái)彌合初始規(guī)范和出帶間的差距。當(dāng)項(xiàng)目開(kāi)始時(shí)，受控隨機(jī)RTL仿真已運(yùn)行好幾天了，但驗(yàn)證工程師仍擔(dān)心會(huì)有“遺漏”的缺陷。被測(cè)RTL設(shè)計(jì)可以實(shí)現(xiàn)視頻和非視頻指令，并用在建項(xiàng)目的算術(shù)模塊來(lái)創(chuàng)建下一代視頻處理芯片。

設(shè)計(jì)驗(yàn)證

驗(yàn)證工作主要集中在21條視頻指令，范圍從“并行轉(zhuǎn)移”到“具有縮小作用的絕對(duì)差”等操作。采用時(shí)序邏輯等效性檢查方法的目標(biāo)是借助用C/C++編寫(xiě)的原始系統(tǒng)模型在芯片級(jí)回歸前改進(jìn)RTL驗(yàn)證。時(shí)序邏輯等效性檢查可以用來(lái)發(fā)現(xiàn)仿真遺漏的缺陷，并改進(jìn)RTL設(shè)計(jì)的調(diào)試工作。

算法模塊的系統(tǒng)模型是用2,391條C/C++語(yǔ)句實(shí)現(xiàn)的。該項(xiàng)目的第一步包含改進(jìn)C/C++代碼使得時(shí)序邏輯等效性檢查器可讀懂它。因該模型最初并非是為等效性檢查編寫(xiě)的，所以其中的一些設(shè)計(jì)構(gòu)造不符合時(shí)序工具語(yǔ)言子集。該項(xiàng)目團(tuán)隊(duì)使用“< ifdef >”語(yǔ)句，來(lái)濾析出沒(méi)有明顯硬件概念的構(gòu)造，例如：“reinterpret cast”和“static cast”。通過(guò)修改C/C++代碼來(lái)實(shí)現(xiàn)這些改變。今后，遵循C/C++開(kāi)發(fā)過(guò)程中的編碼指南后可以不再需要修改設(shè)計(jì)模塊。

設(shè)計(jì)團(tuán)隊(duì)接下來(lái)的工作是設(shè)置驗(yàn)證環(huán)境。時(shí)序邏輯等效性檢查需要在驗(yàn)證前對(duì)復(fù)位狀態(tài)和諸如時(shí)序和接口差異等時(shí)序差異進(jìn)行規(guī)定。時(shí)序差異被具體規(guī)定為I/O映射和設(shè)計(jì)延時(shí)。

針對(duì)用C/C++編寫(xiě)的系統(tǒng)模型，可以通過(guò)添加一個(gè)薄的SystemC“封裝器”來(lái)引入復(fù)位和時(shí)鐘，中間不用改變C/C++模型。

該視頻處理器算法塊的RTL實(shí)現(xiàn)用了4,559行RTL碼，延時(shí)是7個(gè)時(shí)鐘周期。C/C++系統(tǒng)模型的延時(shí)是1個(gè)時(shí)鐘周期，它是由SystemC“封裝器”引入的。設(shè)計(jì)團(tuán)隊(duì)隨后規(guī)定一組新輸入數(shù)據(jù)送至每個(gè)設(shè)計(jì)的頻率。因?yàn)镽TL是管線結(jié)構(gòu)，因此新數(shù)據(jù)是逐個(gè)時(shí)鐘周期輸入的。這樣，C/C++和RTL的吞吐量都是1。

時(shí)序邏輯等效性檢查采用時(shí)序分析和數(shù)學(xué)形式算法來(lái)驗(yàn)證這兩個(gè)模型的全部輸入組合是否一直能得到相同的輸出。與仿真不同，它并行地驗(yàn)證全部輸入條件。在該項(xiàng)目中，相當(dāng)于同時(shí)驗(yàn)證全部指令。因?yàn)槊恳粭l視頻指令實(shí)現(xiàn)一個(gè)具體算法功能，設(shè)計(jì)團(tuán)隊(duì)可以決定一次驗(yàn)證一條視頻指令來(lái)提升調(diào)試效率。

因?yàn)榱私獗粶y(cè)試的指令，所以與同時(shí)對(duì)全部指令進(jìn)行調(diào)試相比，確認(rèn)與任何缺陷相關(guān)的邏輯更加容易。另外，當(dāng)一次只驗(yàn)證一條指令時(shí)，時(shí)序邏輯等效性檢查器運(yùn)行時(shí)運(yùn)行得更快，從而進(jìn)一步提升了調(diào)試效率。

當(dāng)驗(yàn)證第一條指令(VEC4ADD)時(shí)，在RTL模型中發(fā)現(xiàn)了9個(gè)設(shè)計(jì)缺陷、在系統(tǒng)模型中找到1個(gè)缺陷。系統(tǒng)模型中發(fā)現(xiàn)的缺陷可以指導(dǎo)設(shè)計(jì)師如何在以后設(shè)計(jì)中消除C++代碼中的歧義。

時(shí)序邏輯等效性檢查能用10個(gè)或更少時(shí)鐘周期的精簡(jiǎn)反例來(lái)確認(rèn)設(shè)計(jì)差異。對(duì)每個(gè)反例波形來(lái)說(shuō)，產(chǎn)生的波形可以顯示導(dǎo)致設(shè)計(jì)差異的精確輸入序列。

圖：由于RTL是管線結(jié)構(gòu)，新數(shù)據(jù)是逐個(gè)時(shí)鐘周期輸入的。因此C/C++與RTL具體有相同的吞吐量

測(cè)試基準(zhǔn)的再利用

對(duì)每條指令而言，時(shí)序邏輯等效性方法可在5分鐘內(nèi)發(fā)現(xiàn)差異并生成反例。時(shí)序邏輯等效性檢查還將以測(cè)試基準(zhǔn)的方式生成反例，這些反例能與原始C和RTL設(shè)計(jì)一道在仿真時(shí)運(yùn)行。測(cè)試基準(zhǔn)包含監(jiān)視器，因此能暴露以波形方式顯示的相同設(shè)計(jì)缺陷。

在本項(xiàng)目中，反例測(cè)試基準(zhǔn)被復(fù)用為單元級(jí)回歸測(cè)試套件。

在改正VEC4ADD指令代碼中的問(wèn)題后，時(shí)序邏輯等效性檢查器在361秒內(nèi)用52MB證實(shí)了系統(tǒng)模型和RTL間的等效關(guān)系。若對(duì)該指令實(shí)施窮舉仿真，則需運(yùn)行3.7 x 1034個(gè)測(cè)試向量，這樣，即便采用的是1百萬(wàn)周期/秒的仿真器，盡我們一生也難以完成驗(yàn)證。

驗(yàn)證第一條指令(VEC4ADD)所需的全部工作歷時(shí)4天，其中包括設(shè)置時(shí)間、對(duì)多個(gè)設(shè)計(jì)缺陷的調(diào)試及取得完全確認(rèn)的時(shí)間。第二條指令利用與第一條指令相同的設(shè)置腳本，從而允許設(shè)計(jì)師立即投入調(diào)試。他們可以在兩天內(nèi)對(duì)第二條指令(VEC2ADD)的10個(gè)缺陷進(jìn)行查找、糾錯(cuò)及糾錯(cuò)后的確認(rèn)。通過(guò)推斷，全部驗(yàn)證這21條指令需5到7周時(shí)間，實(shí)際用時(shí)取決于發(fā)現(xiàn)的缺陷數(shù)量。當(dāng)采用基于仿真的驗(yàn)證方法時(shí)，設(shè)計(jì)團(tuán)隊(duì)完成相同驗(yàn)證工作需要花6個(gè)月的時(shí)間。

驗(yàn)證結(jié)果

使用系統(tǒng)模型完成圖形指令的RTL驗(yàn)證是成功的?？偣舶l(fā)現(xiàn)了19個(gè)功能缺陷。借助簡(jiǎn)練的反例，時(shí)序邏輯等效性檢查方法可以改進(jìn)驗(yàn)證質(zhì)量、縮短調(diào)試周期。找到的缺陷包括：不正確的符號(hào)擴(kuò)展、遺漏的箝位邏輯以及初始化錯(cuò)誤等，這些缺陷將導(dǎo)致圖像質(zhì)量的降低、軟件設(shè)計(jì)反復(fù)或芯片返工。

時(shí)序邏輯等效性檢查方法能夠借助用C/C++或SystemC編寫(xiě)的系統(tǒng)模型發(fā)現(xiàn)缺陷和驗(yàn)證RTL實(shí)現(xiàn)。它無(wú)需額外的測(cè)試基準(zhǔn)或斷言就能提升功能驗(yàn)證效率。通過(guò)識(shí)別難以發(fā)現(xiàn)的缺陷以及那些被傳統(tǒng)仿真方法遺漏的缺陷，時(shí)序邏輯等效性檢查方法能把設(shè)計(jì)風(fēng)險(xiǎn)降至最小。