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

測(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編寫的系統(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)降至最小。