Global Sources
電子工程專輯
 
電子工程專輯 > EDA/IP
 
 
EDA/IP  

運用等效性檢查驗證連續改變

上網時間: 2006年06月01日     打印版  Bookmark and Share  字型大小:  

關鍵字:IIC  Equivalency checking  sequential changes  等效檢查  驗證 

為滿足對功率、性能和面積的要求,系統單晶片(SoC)和處理器設計團隊正面臨挑戰。隨著晶片複雜度的增加,設計團隊必須驗證上千行的程式碼以獲得設計信心。為了取得成功,設計團隊必須在緊迫的產品上市時間內達到系統目標和驗證標準。

設計信心的增加與獨特測試序列的數量和系統級測試完整性呈函數關係。隨著RTL修改的減少,功能驗證投入增加,因而產生一種‘已測試’模組。此時,模擬測試工具要花幾天或幾周時間完成,且對設計改變非常敏感。功能驗證中的確認要用數以億計的模擬向量才能實現,而這是設計工程師在接近設計末期時都拒絕改變的主要原因。

然而,若最初的佈局和佈線結果顯示設計無法滿足系統時序或功率目標怎麼辦?經過評估,設計工程師可能得出結論:透過對數據路徑的檢查,或許需要控制邏輯。這可能是一個簡單的改變或一次重要的重寫。恐懼之處在於重新驗證經修改的設計需要多少工作,且所有改變將使過去的功能驗證投資付諸流水。

在這些情況下,大多數工程師主張盡可能最少的侵入性改變。然而,這可能引起問題:在全局環境下簡單修正局部實現上變得複雜,或者使風險最小的修正可能不完全滿足系統標準,且需要多次反覆改變。對RTL的任何改變,無論有多小,都可能導入細微的負面影響。

連續改變(sequential change)

在大多數情況下,設計工程師透過把微架構轉換到RTL程式碼來滿足時序、功率和面積目標,微架構轉換是連續的修改。當RTL模型經歷最佳化時,設計工程師對關鍵設計功能如快取記憶體大小、管線(pipeline)的數量和功率管理執行‘what-if’分析。

在SoC和處理器設計中,功率、時序和面積特性難以評估和折衷。可供選擇的微架構具有大量不同的數據路徑,而控制邏輯的實現需要付出大量的工作進行開發和驗證。

圖1:Averaged設計。

模擬可以被用於驗證微架構的最佳化。然而,模擬測試工具要執行數周,而連續的改變可能讓現有的測試基準(testbench)失效。測試基準的效用因為設計延遲、吞吐量或I/O訊號的差異性而降低。當產生這種情況時,測試基準需要手動檢查和調整。

在許多情況下,測試基準比設計還要複雜,使測試基準的改變易受其自身缺陷的影響。根據情況,測試基準故障可能從模組級變化到子系統,或者甚至系統級測試。設計團隊可以透過使用異動或是握手介面撰寫測試基準,將連續改變所帶來的影響局部化。

連續等效檢查為設計工程師提供了另一種功能性驗證選項。透過證明具有連續差異設計之間的等效,所有早先的功能驗證投入都可運用於未來RTL的多種實現。連續等效檢查確保微架構變換的功能正確性,讓設計工程師有信心進行設計後期的RTL改變。該技術也提供了對副作用的快速檢測方法,並確保RTL最佳化與原始功能意圖保持一致。

連續改變的實例

一個邏輯設計、模組或整個晶片可以看作由連續狀態(或記憶體)和組合邏輯構成的機器(machine)。組合邏輯負責計算下一個機器狀態,該狀態是任一時間點的輸入和目前機器狀態的函數。機器輸出是該時間點的目前狀態和/或輸入的函數,乃是根據該邏輯是由moore機器還是由Mealy機器構成而定。

圖1描繪的設計有四個輸入值,它輸出四個值的平均值及輸入值3與平均值的絕對差。透過RTL程式碼、電路圖和狀態時序圖完全描述了該設計。圖1中Average4設計表示有一個狀態級,即輸出上的暫存器。

改變該設計以連續地讀取輸入數值就會修改狀態和時序。這個連續變換是一個簡單連續修正的例子。圖2所示為Average4設計連續輸入實現,請注意到用於儲存輸入所加的暫存器、有限狀態機(FSM),以及相應的輸出延遲。

在我們的例子中,圖2中Average4設計在功能上等效於圖1中的Average4設計。假設採用相同的輸入序列,如果從一致的狀態開始,經過一段時間兩個設計都產生相同的輸出,那麼這一對設計被判定為等效。

在該例子中,簡單的檢查顯示在圖1週期N中的採樣輸出與在圖2週期(N*4)+1中的輸出匹配。這個例子證明,功能上等效的設計可能實質上存在組合邏輯及儲存和存取狀態方式上的差異。

連續變換以改善功率

隨著晶片的日益複雜,需要在性能、面積和功率三者之間進行折衷。隨著設計從系統級向閘級轉移,對動態功率的影響逐漸減少。因此,改善動態功率的設計改變就是典型的連續改變,例如時脈閘控和運算子共享最佳化。

隨著變化範圍的增加,導入細微副作用的可能性增加。因此,要避免在設計過程後期做類似連續改變的重大修改,即使它們節省很大。這樣可避免在向功率最佳化設計收斂的過程中產生嚴重的侷限性,因為精確的功率估計需要佈局和佈線的電容器資訊。

下一個例子顯示了用於改善功率的Average4控制邏輯中的連續改變。功率的降低透過利用共享資源和修改狀態機編碼以圍繞單一加法器和暫存器迴圈來實現。圖3所示為經過功率最佳化的Average4設計。

功率管理開始於系統級,系統級模型執行要足夠快以啟動作業系統和執行應用追蹤(application trace)。這給出了開關行為的精確估計,系統級模型然後被最佳化為RTL實現。

RTL模型具有相同的功能,且可以考慮像電容器這樣的實體實現細節以進一步分析動態功率。有了功能精確的系統級模型就允許在系統級描述和RTL實現之間進行連續等效檢查。

連續變換以改善時序

時序和長路徑是常見的RTL設計問題。儘管改善時序的改變可能簡單,可是設計過程後期的驗證成本卻相當高。

考慮一種改善時序的最小入侵性RTL改變,數據路徑邏輯圍繞管線觸發器重定時序。這個連續改變解決了邊際時序問題,並不大可能影響模擬測試基準。然而,傳統的組合等效檢查器無法處理重定時序邏輯,因為觸發器不再被認為是等效的設計點。

在圖4中,我們圍繞在Average4設計中的狀態單元對組合邏輯重定時序。為簡化起見,在時序波形中的週期長度被縮短,並且在加法器、減法器、比較器和再使用邏輯之間的詳細暫存器佈局從圖中被省略。這些改變的最終增強了整個系統性能,而其功能與原始Average4設計相同。

圖2:Averaged4電路的連續實現。

當簡單的重定時序達不到時序收斂時,需要做更大膽的連續改變。在此情況下,可能有必要增加管線級數。

重定時序RTL控制邏輯的特性造成一些非常難以驗證的問題,經常導入邊際缺陷(corner case bug)。例如,在CPU設計中,對管理指令級管線和多執行緒的控制邏輯進行連續重定時,會導致不僅難以除錯而且難以模擬的活鎖(live-lock)及其它錯誤。基於驗證方法的模擬必須解決反應時間和吞吐量差異的問題,又要增加定向和隨機測試來解決控制邏輯連續改變的問題。

為了避免使測試工具重新生效來解決輸出中的額外延遲,測試基準應該用反應時間可程式或反應遲鈍的介面來寫。設計工程師必須提前計劃連續改變的驗證,否則的話,這種日益增加的普通設計改變會對計畫進度和成本造成負面影響。

連續等效檢查

設計工程師快速處理連續改變驗證的方法之一是利用連續等效檢查器(sequential equivalency checker)。連續等效檢查器驗證新的RTL實現在功能上等效於早先已驗證的參考設計,而不管狀態、介面或連續微架構差異的變化。一個連續等效檢查器可以在數分鐘內檢測出設計差異(如果存在的話),立即向設計工程師提供關於RTL改變的反饋。不依賴於測試基準或工具,連續等效檢查利用一個用VerilogVHDL、SystemC或C/C++寫成的RTL黃金模型或系統級參考設計。與組合等效檢查器不同,連續檢查器證明跨連續級和數據抽象的功能等效性。像重定時序和資源共享這樣的連續改變僅需要較小的變化來設置參數以反映新的時序資訊。

本文小結

對功率、時序和面積的微架構最佳化經常會導致RTL數據路徑和控制邏輯的連續改變。連續改變對功能驗證有相當大的影響。它們不僅需要對整個設計進行仔細的重新驗證,而且它們還會令模擬測試基準失效。設計團隊發現他們本身已陷入完成系統級要求、最小化設計改變和功能驗證完整性的重圍之中。

在設計過程後期的連續改變會更加普遍,設計工程師應該透過壓縮測試基準介面並利用連續等效檢查來改善其功能驗證。連續等效檢查不用測試基準就可以驗證設計、快速識別設計負面影響,並自然地用連續差異處理設計。

最後,能夠滿懷信心地做出和驗證連續改變,會大幅地提高設計工程師在做系統最佳化時的工作效率,並使設計團隊能夠滿足其迫切的功率、時序和面積目標。

作者: Mitch Dale

產品市場總監

Duncan MacKay

方法學顧問

Venkat Krishnaswami

工程總監

Calypto Design Systems公司




投票數:   加入我的最愛
我來評論 - 運用等效性檢查驗證連續改變
評論:  
*  您還能輸入[0]個字
*驗證碼:
 
論壇熱門主題 熱門下載
 •   將邁入40歲的你...存款多少了  •  深入電容觸控技術就從這個問題開始
 •  我有一個數位電源的專利...  •  磷酸鋰鐵電池一問
 •   關於設備商公司的工程師(廠商)薪資前景  •  計算諧振轉換器的同步整流MOSFET功耗損失
 •   Touch sensor & MEMS controller  •  針對智慧電表PLC通訊應用的線路驅動器
 •   下週 深圳 llC 2012 關於PCB免費工具的研討會  •  邏輯閘的應用


EE人生人氣排行
 
返回頁首