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

測試基準的再利用

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

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

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

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

驗證結果

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

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