寄存器傳輸級（RTL）驗證在數字硬件設計中仍是瓶頸。行業調研顯示，功能驗證占整個設計工作的70%.但即使把重點放在驗證上面，仍有超過60%的設計出帶需要返工。其主要原因是在功能驗證過程中暴露出來的邏輯或功能瑕疵和缺陷等。顯然，需要進一步改進驗證技術。

設計團隊一般采用系統模型進行驗證。就驗證來說，系統模型比RTL更具優勢，比如系統模型易于開發且具有優異的運行時性能。挑戰性在于如何在系統級驗證和生成功能正確的RTL間建立起橋梁。一種稱為時序邏輯等效性檢查的方法具有橋接兩者的能力，它是基于C/C++或SystemC編寫的規范來對RTL實現進行形式驗證。

本文將討論商用圖形處理芯片所采用的從系統級到RTL的設計和驗證流程。在該流程中，先要開發出系統模型，然后用它來確認視頻指令的算術運算，然后再采用時序邏輯等效性檢查方法驗證RTL實現。

系統級流程

隨著設計復雜性的增加，為了仿真整個系統，系統級建模變得不可避免。伴隨功能劃分、模塊接口和硬件/軟件協同設計而來的設計復雜性呈指數形式增長，使得系統驗證勢在必行。目前常采用C/C++或SystemC進行系統級設計和驗證。

本例采用了C/C++來建模視頻處理算法模塊。一旦系統模型完成了調整和驗證，RTL設計師就可以編寫Verilog代碼。高層綜合工具可以從系統代碼生成RTL.但工程師更常見的做法是用RTL代碼手工重新編寫設計。它是設計的解釋而非轉換。即便已用多種驗證測試平臺對RTL實現進行了驗證，采用基于仿真的方法也無法測試全部可能的狀態。

在設計流程中有許多驗證工具和方法可以采用，它們包括：基于斷言的驗證，隨機激勵生成和以覆蓋率驅動的驗證等。上述方法在功能上也許是值得依賴的，但它們都沒有借助系統模型。時序邏輯等效性檢查方法可以將系統模型的這種信心直接轉換為RTL實現。

圖形處理器市場受成像質量、再現性能和用戶購買時機的影響很大。對負責研制最新圖形處理器芯片的項目團隊來說，上述因素要求他們迅速開發出新算法、拿出新設計。為了滿足這種要求，可以采用系統模型來彌合初始規范和出帶間的差距。當項目開始時，受控隨機RTL仿真已運行好幾天了，但驗證工程師仍擔心會有“遺漏”的缺陷。被測RTL設計可以實現視頻和非視頻指令，并用在建項目的算術模塊來創建下一代視頻處理芯片。

設計驗證

驗證工作主要集中在21條視頻指令，范圍從“并行轉移”到“具有縮小作用的絕對差”等操作。采用時序邏輯等效性檢查方法的目標是借助用C/C++編寫的原始系統模型在芯片級回歸前改進RTL驗證。時序邏輯等效性檢查可以用來發現仿真遺漏的缺陷，并改進RTL設計的調試工作。

算法模塊的系統模型是用2,391條C/C++語句實現的。該項目的第一步包含改進C/C++代碼使得時序邏輯等效性檢查器可讀懂它。因該模型最初并非是為等效性檢查編寫的，所以其中的一些設計構造不符合時序工具語言子集。該項目團隊使用“< ifdef >”語句，來濾析出沒有明顯硬件概念的構造，例如：“reinterpret cast”和“static cast”.通過修改C/C++代碼來實現這些改變。今后，遵循C/C++開發過程中的編碼指南后可以不再需要修改設計模塊。

設計團隊接下來的工作是設置驗證環境。時序邏輯等效性檢查需要在驗證前對復位狀態和諸如時序和接口差異等時序差異進行規定。時序差異被具體規定為I/O映射和設計延時。

針對用C/C++編寫的系統模型，可以通過添加一個薄的SystemC“封裝器”來引入復位和時鐘，中間不用改變C/C++模型。

該視頻處理器算法塊的RTL實現用了4,559行RTL碼，延時是7個時鐘周期。C/C++系統模型的延時是1個時鐘周期，它是由SystemC“封裝器”引入的。設計團隊隨后規定一組新輸入數據送至每個設計的頻率。因為RTL是管線結構，因此新數據是逐個時鐘周期輸入的。這樣，C/C++和RTL的吞吐量都是1.

時序邏輯等效性檢查采用時序分析和數學形式算法來驗證這兩個模型的全部輸入組合是否一直能得到相同的輸出。與仿真不同，它并行地驗證全部輸入條件。在該項目中，相當于同時驗證全部指令。因為每一條視頻指令實現一個具體算法功能，設計團隊可以決定一次驗證一條視頻指令來提升調試效率。

因為了解被測試的指令，所以與同時對全部指令進行調試相比，確認與任何缺陷相關的邏輯更加容易。另外，當一次只驗證一條指令時，時序邏輯等效性檢查器運行時運行得更快，從而進一步提升了調試效率。

當驗證第一條指令（VEC4ADD）時，在RTL模型中發現了9個設計缺陷、在系統模型中找到1個缺陷。系統模型中發現的缺陷可以指導設計師如何在以后設計中消除C++代碼中的歧義。

時序邏輯等效性檢查能用10個或更少時鐘周期的精簡反例來確認設計差異。對每個反例波形來說，產生的波形可以顯示導致設計差異的精確輸入序列。

圖：由于RTL是管線結構，新數據是逐個時鐘周期輸入的。因此C/C++與RTL具體有相同的吞吐量

測試基準的再利用

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

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

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

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

驗證結果

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

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