基于時序邏輯等效性檢查方法的RTL驗證

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

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

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

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

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

驗證結(jié)果

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

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