oC開發(fā)來說,巨大的掩膜制造成本要求首次流片取得成功。急劇增加的驗(yàn)證復(fù)雜度與日益縮短的上市時(shí)間也敦促業(yè)界尋找更加有效和自動(dòng)化的驗(yàn)證方法。
形式驗(yàn)證(FV)的自動(dòng)化就是以上問題的一種可行解決方案。作為成熟的偽隨機(jī)驗(yàn)證技術(shù)的補(bǔ)充,FV讓驗(yàn)證工程師(或設(shè)計(jì)師)能夠?qū)﹄娐返奶囟ú糠诌M(jìn)行詳盡的驗(yàn)證。本文將討論OCP等總線協(xié)議的自動(dòng)化形式驗(yàn)證。
屬性的概念
為了對(duì)任意IP進(jìn)行形式驗(yàn)證,設(shè)計(jì)師或驗(yàn)證工程師必需從該IP的規(guī)范中提取各種屬性。每一種屬性描述了該IP的一個(gè)或多個(gè)特點(diǎn)。最好是先提取高層的系統(tǒng)屬性,因?yàn)檫@些屬性每個(gè)都涵蓋了該IP的一組特點(diǎn)。低層的屬性接近RTL,因此往往被證明用處不大。
設(shè)計(jì)師提取出的每一種屬性均可以被形式驗(yàn)證工具(例如Cadence的Incisive Formal Verifier)用作斷言(檢查)或假設(shè)(環(huán)境約束)。大多數(shù)時(shí)候,假設(shè)被施加到待測設(shè)計(jì)(DUT)的輸入端,斷言則被施加于DUT的輸出端。例如在OCP協(xié)議中有一個(gè)屬性,它規(guī)定應(yīng)答狀態(tài)只能在出現(xiàn)相應(yīng)的請求狀態(tài)之后啟動(dòng)。在驗(yàn)證帶OCP從接口的IP(見圖1)時(shí),該屬性就被用作斷言(檢查),因?yàn)閼?yīng)答狀態(tài)是該IP的一個(gè)輸出。
圖1:驗(yàn)證帶OCP從接口的IP。
OCP協(xié)議的形式驗(yàn)證
在驗(yàn)證帶一個(gè)或一個(gè)以上OCP接口的IP時(shí),理論上只需簡單地提取其OCP屬性,并對(duì)其進(jìn)行形式上的檢驗(yàn)即可,但實(shí)際情況并非如此。形式驗(yàn)證中最困難的部分在于OCP規(guī)范的復(fù)雜性。OCP接口極強(qiáng)的可配置性讓我們能夠創(chuàng)建一個(gè)十分靈活的系統(tǒng),但同時(shí)也加大了驗(yàn)證的負(fù)擔(dān)。確定一組合適的OCP屬性非常重要,因?yàn)镺CP屬性的錯(cuò)誤選擇可能導(dǎo)致一些邊界情況被遺漏,從而使驗(yàn)證出現(xiàn)漏洞。
很明顯,要求為所有可能的OCP配置確定一組完整的OCP屬性列表。OCP-IP組織很早就認(rèn)識(shí)到這一需求。為此,OCP-IP功能驗(yàn)證工作小組(FVWG)創(chuàng)建了一個(gè)OCP-IP一致性計(jì)劃(OCP-IP compliance plan)。該計(jì)劃對(duì)所有OCP屬性進(jìn)行了定義,同時(shí)也大致描述了每一個(gè)屬性應(yīng)由哪些配置參數(shù)激活。同樣,在OCP接口配置的基礎(chǔ)上,只有相關(guān)的一組子屬性可以被識(shí)別和證實(shí)。更全面的描述請參考OCP-IP 2.2規(guī)范中的第13、14和15章。
OCP VIP庫
今天的許多高性能SoC(例如德州儀器公司的OMAP多媒體應(yīng)用處理器)都是基于OCP的。在使用時(shí),幾個(gè)主要器件或主要子系統(tǒng)通過基于OCP的連接與多個(gè)從器件(外設(shè)和存儲(chǔ)器等)相連,見圖2。
圖2:利用基于OCP的互連實(shí)現(xiàn)的內(nèi)核底層規(guī)劃。
為了盡可能減少所有這些OCP接口的驗(yàn)證工作量,幾家EDA廠商決定創(chuàng)建一個(gè)OCP VIP庫。這個(gè)庫(見圖3左側(cè))中包含了OCP一致性計(jì)劃中定義的所有屬性,其代碼通常是由一個(gè)或多個(gè)專業(yè)驗(yàn)證工程師采用PSL/SVA+輔助VHDL/Verilog語言編寫的。這種代碼編寫是一次性工作。
圖3:廠商提供的庫與OCP驗(yàn)證環(huán)境的相互作用。
為了選擇一組適合某個(gè)特定OCP接口的子屬性,可以用一個(gè)腳本對(duì)OCP配置文件(即IP_)進(jìn)行解析。最終被選出的一組屬性可被形式驗(yàn)證工具用作斷言或假設(shè)。
這個(gè)VIP庫中還包含了很大的一組cover。這組cover可以檢測出過份約束的環(huán)境,因此特別重要。此外,cover還能幫助檢測到虛警狀態(tài)(即沒有滿足條件時(shí)出現(xiàn)的斷言),從而可以避免出現(xiàn)無意義的錯(cuò)誤。
最后,不要低估開發(fā)一套魯棒性協(xié)議VIP的重要性。盡管OCP-IP定義屬性的工作做得不錯(cuò),但在實(shí)現(xiàn)時(shí)仍可能出現(xiàn)大量問題(例如PCL、輔助Verilog甚至屬性子集選擇解析器中的錯(cuò)誤)。這些問題直接表明一個(gè)庫必需經(jīng)過嚴(yán)格測試,在測試階段,該庫被應(yīng)用于具有不同配置的多個(gè)IP。大型EDA廠商通常很適合這一工作,因?yàn)樗麄兺鶕碛泻艽蟮膬?nèi)部IP回歸數(shù)據(jù)庫。通常要配合工業(yè)客戶進(jìn)行詳盡的測試才能完成整個(gè)測試過程。
TI提供的一些OCP VIP經(jīng)驗(yàn)
圖4:Cadence的OCP協(xié)議VIP集成到TI的設(shè)計(jì)中。
如圖4所示,在TI法國公司的無線終端業(yè)務(wù)部門(WTBU),我們可以輕松將Cadence的OCP協(xié)議VIP集成到我們內(nèi)部的設(shè)計(jì)流程中。從下圖可以看出,必須要定義的(模板)文件只有:
·.f: 用于驅(qū)動(dòng)IFV
·.tcl:用于初始化電路
·.psl:用于對(duì)非OCP的主要輸入(如復(fù)位、測試和電源管理)建模
而用戶只需要:
·調(diào)用一個(gè)Makefile目標(biāo)對(duì)RTL進(jìn)行分析和詳細(xì)描述
·調(diào)用一個(gè)Makefile目標(biāo)來解析IP_并獲取正確的子集
·編輯模板文件(.f/.tcl/.psl)
·最后利用IFV執(zhí)行形式驗(yàn)證,以檢驗(yàn)OCP的一致性
為了讓讀者對(duì)驗(yàn)證流程的簡單性與有效性有一個(gè)大致的了解,請看以下例子。工程師在驗(yàn)證一個(gè)帶基本從OCP接口的IP時(shí)平均要用30分鐘到1個(gè)小時(shí)的時(shí)間。其中大部分時(shí)間都用于編寫設(shè)置主要輸入約束的PSL模板文件。需要注意的是,這是100%徹底驗(yàn)證的結(jié)果。更加傳統(tǒng)的偽隨機(jī)仿真環(huán)境則要求將OCP eVC實(shí)例化,編寫隨機(jī)測試用例,最重要的是對(duì)功能覆蓋率進(jìn)行嚴(yán)格定義。由于功能覆蓋的定義存在一些差異,因此動(dòng)態(tài)回歸在OCP接口驗(yàn)證時(shí)很可能會(huì)遺漏一些邊界條件。我們發(fā)現(xiàn)在許多模塊的動(dòng)態(tài)仿真中常被遺漏的邊界條件是,在OCP傳輸仍未完成時(shí)IP就經(jīng)歷軟件復(fù)位情況下的OCP接口行為。此外,在具備多個(gè)OCP接口的模塊中,如果一個(gè)接口用于配置模塊,另一個(gè)用于傳輸實(shí)際數(shù)據(jù)流,那么在采用基于偽隨機(jī)的仿真方法時(shí)也容易出錯(cuò)和留下缺陷。最后一個(gè)同時(shí)也很難找到的缺陷是FSM死鎖,這種缺陷用形式驗(yàn)證的方式比用偽隨機(jī)仿真的方式更容易發(fā)現(xiàn)。
我們在多個(gè)無線OMAP項(xiàng)目中采用了OCP VIP方法,每個(gè)項(xiàng)目中約有50個(gè)IP,每個(gè)IP具備一個(gè)或一個(gè)以上的OCP接口。結(jié)果我們發(fā)現(xiàn)的問題涵蓋了從難以發(fā)現(xiàn)的邊界條件到結(jié)構(gòu)性缺陷很大的范圍。
利用協(xié)議VIP進(jìn)行較高層特性的形式驗(yàn)證
一個(gè)IP通常包含:一個(gè)clk & rst接口、一個(gè)電源管理(PM)接口、一個(gè)用于配置其內(nèi)部寄存器的接口,以及一個(gè)或多個(gè)用于與外界(串行協(xié)議或存儲(chǔ)器)通信的功能總線。
對(duì)于SoC中常用的標(biāo)準(zhǔn)協(xié)議來說,很可能存在相應(yīng)的協(xié)議VIP(OCP,AXI,AHB)。而對(duì)于一些內(nèi)部協(xié)議而言,相應(yīng)的VIP(例如電源管理)也是可以開發(fā)的。通過使用這些VIP(見圖5),驗(yàn)證工程師既獲得了“自由”環(huán)境,也得到了“自由”的低層協(xié)議檢查。
5:協(xié)議VIP可以改善驗(yàn)證環(huán)境。
在此基礎(chǔ)上,工程師又可以編寫更高層次的系統(tǒng)屬性。最佳情況下,系統(tǒng)級(jí)的屬性甚至無需對(duì)遺漏的接口(func1 & func2)進(jìn)行建模就能得到驗(yàn)證。這時(shí)的驗(yàn)證更加抽象,因?yàn)樗窃诩s束不足的環(huán)境下進(jìn)行的。但如果反例顯示出現(xiàn)了有效的違例情況,那么就必須對(duì)剩下的接口進(jìn)行建模。
我們開發(fā)的一些最常用的高層屬性例子包括:
·通過橋接進(jìn)行分組轉(zhuǎn)換
·存儲(chǔ)器和緩存的一致性
·性能和延遲屬性
·數(shù)據(jù)完整性(該屬性不是很適合形式驗(yàn)證但仍值得一試)
本文小結(jié)
采用VIP進(jìn)行自動(dòng)化形式協(xié)議驗(yàn)證能使關(guān)鍵IP接口得到快速詳盡的驗(yàn)證。VIP庫在編寫和測試之后可用于改善驗(yàn)證質(zhì)量并縮短驗(yàn)證時(shí)間。由于最后的VIP提供了一個(gè)“自由”的環(huán)境,因而還能用于簡化高層系統(tǒng)性能的驗(yàn)證。
作者:Jeroen Vliegen
WTBU部門形式驗(yàn)證工程師
TI法國公司
