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

基於OCP IP核心的自動化形式驗證

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

關鍵字:形式驗證  屬性  聲明 

對於今天的SoC開發來說,巨大的光罩製造成本要求首次投片取得成功。急劇增加的驗證複雜度與日益縮短的上市時間也敦促業界尋找更加有效和自動化的驗證方法。

形式驗證(FV)的自動化就是以上問題的一種可行解決方案。作為成熟的偽隨機驗證技術的補充,FV讓驗證工程師(或設計師)能夠對電路的特定部份進行詳盡的驗證。本文將討論OCP等匯流排協議的自動化形式驗證。

屬性的概念

為了對任意IP進行形式驗證,設計師或驗證工程師必須從該IP的規格中擷取各種屬性。每一種屬性描述了該IP的一個或多個特點。最好是先擷取高層的系統屬性,因為這些屬性每個都涵蓋了該IP的一組特點。低層的屬性接近RTL,因此往往被證明用處不大。

設計師擷取出的每一種屬性均可以被形式驗證工具(例如Cadence的Incisive Formal Verifier)作為聲明(檢查)或假設(環境約束)。大多數時候,假設被施加到待測設計(DUT)的輸入端,聲明則被施加於DUT的輸出端。例如在OCP協議中有一個屬性,它規定應答狀態只能在出現相應的請求狀態之後啟動。在驗證帶OCP從介面的IP(見圖1)時,該屬性就被作為聲明(檢查),因為應答狀態是該IP的一個輸出。

圖1:驗證帶OCP從介面的IP。
圖1:驗證帶OCP從介面的IP。

OCP協議的形式驗證

在驗證帶一個或一個以上OCP介面的IP時,理論上只需簡單地擷取其OCP屬性,並對其進行形式上的檢驗即可,但實際情況並非如此。形式驗證中最困難的部份在於OCP規格的複雜性。OCP介面極強的可配置性讓我們能夠製作一個十分靈活的系統,但同時也加大了驗證的負擔。確定一組合適的OCP屬性非常重要,因為OCP屬性的錯誤選擇可能導致一些邊界情況被遺漏,使驗證出現漏洞。

很明顯,要求為所有可能的OCP配置確定一組完整的OCP屬性列表。OCP-IP組織很早就認識到這一需求。為此,OCP-IP功能驗證工作小組(FVWG)製作了一個OCP-IP一致性計劃(OCP-IP compliance plan)。該計劃對所有OCP屬性進行了定義,同時也大致描述了每一個屬性應由哪些配置參數啟動。同樣,在OCP介面配置的基礎上,只有相關的一組子屬性可以被識別和證實。更全面的描述可參考OCP-IP 2.2規格中的第13、14和15章。

圖2:利用基於OCP的互連實現的核心底層規劃。
圖2:利用基於OCP的互連實現的核心底層規劃。

OCP VIP庫

今天的許多高性能SoC(例如德州儀器公司的OMAP多媒體應用處理器)都是基於OCP的。在使用時,幾個主要元件或主要子系統透過基於OCP的連接與多個從元件(週邊和記憶體等)相連,見圖2。

為了盡可能減少所有這些OCP介面的驗證工作量,幾家EDA廠商決定製作一個OCP VIP庫。這個庫(見圖3左側)中包含了OCP一致性計劃中定義的所有屬性,其程式碼通常是由一個或多個專業驗證工程師採用PSL/SVA+輔助VHDL/Verilog語言編寫的。這種程式碼編寫是一次性工作。

圖3:廠商提供的庫與OCP驗證環境的相互作用。
圖3:廠商提供的庫與OCP驗證環境的相互作用。

為了選擇一組適合某個特定OCP介面的子屬性,可以用一個腳本對OCP配置文件(即IP_rtl.conf)進行解析。最終被選出的一組屬性可被形式驗證工具作為聲明或假設。

這個VIP庫中還包含了很大的一組cover。這組cover可以檢測出過份約束的環境,因此特別重要。此外,cover還能幫助檢測到虛警狀態(即沒有滿足條件時出現的聲明),可避免出現無意義的錯誤。

最後,不要低估開發一套強韌性協議VIP的重要性。儘管OCP-IP定義屬性的工作做得不錯,但在實現時仍可能出現大量問題(例如PCL、輔助Verilog甚至屬性子集選擇解析器中的錯誤)。這些問題直接顯示一個庫必須經過嚴格測試,在測試階段,該庫被應用於具有不同配置的多個IP。大型EDA廠商通常很適合這一工作,因為他們往往擁有很大的內部IP回歸資料庫。通常要配合客戶進行詳盡的測試才能完成整個測試過程。

TI提供的一些OCP VIP經驗

圖4:Cadence的OCP協議VIP整合在TI的設計中。
圖4:Cadence的OCP協議VIP整合在TI的設計中。

如圖4所示,在TI法國公司的無線終端業務部門(WTBU),我們可以輕鬆將Cadence的OCP協議VIP整合在我們內部的設計流程中。從下圖可以看出,必須要定義的(模板)文件只有:

• .f: 用於驅動IFV

• .tcl:用於初始化電路

• .psl:用於對非OCP的主要輸入(如重置、測試和電源管理)建模

而用戶只需要:

• 呼叫一個Makefile目標對RTL進行分析和詳細描述

• 呼叫一個Makefile目標來解析IP_rtl.conf並獲取正確的子集

• 編輯模板文件(.f/.tcl/.psl)

• 最後利用IFV執行形式驗證,以檢驗OCP的一致性

為了讓讀者對驗證流程的簡單性與有效性有一個大致的瞭解,請看以下例子。工程師在驗證一個帶基本從OCP介面的IP時平均要用30分鐘到1個小時的時間。其中大部份時間都用於編寫設置主要輸入約束的PSL模板文件。需要注意的是,這是100%徹底驗證的結果。更加傳統的偽隨機模擬環境則要求將OCP eVC實例化,編寫隨機測試用例,最重要的是對功能覆蓋率進行嚴格定義。由於功能覆蓋的定義存在一些差異,因此動態回歸在OCP介面驗證時很可能會遺漏一些邊界條件。我們發現在許多模組的動態模擬中常被遺漏的邊界條件是,在OCP傳輸仍未完成時IP就經歷軟體重置情況下的OCP介面行為。此外,在具備多個OCP介面的模組中,如果一個介面用於配置模組,另一個用於傳輸實際數據串流,那麼在採用基於偽隨機的模擬方法時也容易出錯和留下缺陷。最後一個同時也很難找到的缺陷是FSM死鎖,這種缺陷用形式驗證的方式比用偽隨機模擬的方式更容易發現。

我們在多個無線OMAP計劃中採用了OCP VIP方法,每個計劃中約有50個IP,每個IP具備一個或一個以上的OCP介面。結果我們發現的問題涵蓋了從難以發現的邊界條件到結構性缺陷等極大範圍。

利用協議VIP進行較高層特性的形式驗證

一個IP通常包含:一個clk & rst介面、一個電源管理(PM)介面、一個用於配置其內部暫存器的介面,以及一個或多個用於與外界(串列協議或記憶體)通訊的功能匯流排。

對於SoC中常用的標準協議來說,很可能存在相應的協議VIP(OCP,AXI,AHB)。而對於一些內部協議而言,相應的VIP(例如電源管理)也是可以開發的。透過使用這些VIP(見圖5),驗證工程師既獲得了‘自由’環境,也得到了‘自由’的低層協議檢查。

5:協議VIP可以改善驗證環境。
5:協議VIP可以改善驗證環境。

在此基礎上,工程師又可以編寫更高層次的系統屬性。最佳情況下,系統級的屬性甚至無需對遺漏的介面(func1 & func2)進行建模就能得到驗證。這時的驗證更加抽象,因為它是在約束不足的環境下進行的。但如果反例顯示出現了有效的違例情況,那麼就必須對剩下的介面進行建模。

我們開發的一些最常用的高層屬性例子包括:

• 透過橋接進行封包轉換

• 記憶體和緩衝記憶體的一致性

• 性能和延遲屬性

• 數據完整性(該屬性不是很適合形式驗證但仍值得一試)

本文小結

採用VIP進行自動化形式協議驗證能使關鍵IP介面得到快速詳盡的驗證。VIP庫在編寫和測試之後適用於改善驗證品質並縮短驗證時間。由於最後的VIP提供了一個‘自由’的環境,因此能用於簡化高層系統性能的驗證。

作者:Jeroen Vliegen

WTBU部門形式驗證工程師

TI法國公司





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


EE人生人氣排行
 
返回頁首