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

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

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

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

系統級流程

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

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

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

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

設計驗證

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

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

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

針對用C/C++編寫(xiě)的系統模型，可以通過(guò)添加一個(gè)薄的SystemC“封裝器”來(lái)引入復位和時(shí)鐘，中間不用改變C/C++模型。

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

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

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

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

時(shí)序邏輯等效性檢查能用10個(gè)或更少時(shí)鐘周期的精簡(jiǎn)反例來(lái)確認設計差異。對每個(gè)反例波形來(lái)說(shuō)，產(chǎn)生的波形可以顯示導致設計差異的精確輸入序列。

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