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

測試基準的再利用

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

在本項目中，反例測試基準被復用為單元級回歸測試套件。

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

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

驗證結果

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

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