一種基于測例層模型的功能驗證方法*

謝 崢,王明江*,雍珊珊,王新安

(1.電子與信息工程學院,哈爾濱工業大學深圳研究生院,廣東 深圳 518055;2.信息工程學院,北京大學深圳研究生院,廣東 深圳 518055)

一種基于測例層模型的功能驗證方法*

謝 崢1,王明江1*,雍珊珊2,王新安2

(1.電子與信息工程學院,哈爾濱工業大學深圳研究生院,廣東 深圳 518055;2.信息工程學院,北京大學深圳研究生院,廣東 深圳 518055)

針對集成電路功能驗證的完整性和重用性問題,使用測例層模型,構建協議功能完整覆蓋的驗證計劃,并使用UVM驗證方法和庫函數搭建驗證環境,對一款符合GJB 800/900 MHz RFID芯片系統的設計進行功能驗證。所提出的測例層模型具備通用性。填充協議內容后的模型,在滿足相同協議的設計之間可重用,在相似協議或非完整協議的設計中也可重用,即面向協議的測例層VIP及其構建方法。最終保證了GJB協議芯片的驗證覆蓋率,在TSMC 0.18 μm工藝流片成功。

功能驗證;測例層模型;RFID;UVM

隨著超大規模集成電路制造工藝技術向14 nm、10 nm[1]、甚至7 nm[2]的進步,集成電路設計復雜度也不斷提高,SoC的驗證工作已經占據了約70%的設計時間[3],迫切需要功能驗證方面新方法學的指導。從2000年的e語言的誕生,到eRM可重用方法學、基于vera語言的RVM方法學、基于SystemVerilog和SystemC的AVM方法學、VMM方法學、URM方法學、OVM方法學,再到現在主流公司全部支持的UVM方法,可以看出以重用性來提高功能驗證效率的方法得到了較好的發展。然而驗證重用性仍然具有3個緯度的發展空間:從SoC到衍生產品的重用;從IP到SoC的重用;不同抽象級別在架構、設計、軟件、驗證等混合平臺上的重用[4]。

功能驗證的本質是保證設計功能的正確性,由于設計的復雜度限制了完整功能描述的形式化定義,以及形式驗證方法對其進行檢查的范圍,所以需要“完整”的功能測試集合的支持。然而“完整”的功能測試集合實際中是以約束隨機和定向相結合來實現的?；诜抡娴尿炞C,包括testcase和testbench,基于UVM的方法在testbench層較好的支持了各細分層次(場景層、功能層、命令層、信號層等)的組件以及功能覆蓋率的定義和收集過程,形成了較完整的框架結構。testcase層是面向內容的層次,直接和功能測試用例、功能覆蓋點、功能參考模型相關。在基于標準協議的設計中使用黑盒驗證的方式時,testcase層的內容具有在3個緯度上更廣泛的重用性。

本文提出了在testcase層的模型,通過對模型進行協議內容的填充和建模,產生完整的功能測試用例、完整的功能覆蓋點、完整的功能參考模型。首先對自然語言的功能描述或標準協議向模型進行填充和映射,再從模型向驗證環境中的相關組件進行內容上的映射和轉化,從而實現了對功能驗證完整性和重用性的保證。再配合testbench層的UVM方法,在GJB 800/900 MHz RFID芯片系統設計項目中,保證了流片的成功。

1 功能驗證的基本原理

待驗證設計(DUV)的功能模型是一個功能集合F,由fi函數作為元素組成,其中fi以輸入集合U為參數,U由變量uj組成,對于fi函數可以使用U的子集Ui,如式(1)～式(3)。

F={fi(U)},i∈{1,…,I}

(1)

U={uj},j∈{1,…,J}

(2)

fi(Ui),Ui?U

(3)

在輸入集合為非離散的或離散的巨大空間時,對函數fi的輸入遍歷在基于仿真的驗證中是不實際的。從功能角度,功能覆蓋矩陣(FCM)是覆蓋率驅動的驗證(CDV)的基礎。功能覆蓋率矩陣的關鍵在于切分和組合。對變量uj的取值集合Sj進行劃分,劃分成Dj個子集。那么對于擁有L個變量的fi函數的組合數就有C(fi)個,如式(4)、式(5)所示。

Sj=Sj(1)∪Sj(2)∪…∪Sj(Dj)

(4)

(5)

當驗證fi函數時,測例遍歷所有C(fi)個組合。對于其中一種組合Vk(fi),其各變量uj的值為v(uj),v(uj)從Sj(d(k))子集中隨機選擇,且d(k)是Vk(fi)這種組合與變量uj的取值集合Sj的分組之間的關系。在約束隨機驗證中,d(k)是一種約束,如式(6)～式(7)。

Vk(fi)={v(uj)},uj∈Ui,k=1,…,C(fi)

(6)

v(uj)=rand(Sj(d(k))),d(k)=1,2,…Dj

(7)

在細化的過程中,U對應testbench中的組件,比如driver、receiver、stimulator、responder等[5]。文獻[5]中使用了簡單的線性劃分器,使各子集的大小相等,即

Sj(a)∩Sj(b)=φ,a,b=1,2,…Dj, ifa≠b

(8)

如果輸入存在相關性,對變量uj的取值集合Sj的劃分則不嚴格遵守式(8),遵守式(4),在這種情況下一些組合成為非法的,所以

(9)

功能集合F對fi(U)函數的選擇是對DUV的配置,帶有分段函數的特點。下標i在fi(U)中可以被看作是輸入集合U的一部分。在分層的驗證環境的頂層,其表現為場景的設置過程。

根據抽象層次,輸入集合U演變成了transaction或信號中的參數或者向量。DUV的功能模型可以被擴展出一個順序性的維度,或一個結構性的維度。當引入時間參數t后,式(1)被描述成

F(t)={fi(U)},i∈{1,…,I}

(10)

當t被忽略時,F是一個用來處理應用數據包的算法模型,或一個處理總線transaction的程序設計員視角的模型,由transaction事件觸發。當t被粗略的時間化后,F(t)成為了一個總線周期精確的模型,或程序設計員視角加時間的模型。當t被周期精確化后,F(t)成為一個周期精確的模型,由時鐘信號觸發。所以式(6)可以轉化為

Vt,k(fi)={v(uj)},
uj∈Uik=1,…,C(fi)t=t1,t2,…

(11)

式中:時間點基于觸發事件。一個輸入序列Seq表示為

Seqt1,tn=Vt1,k(fi),Vt2,k(fi),…,Vtn,k(fi)n=1,2,…

(12)

=>F(t1),F(t2),…,F(tn)n=1,2,…

(13)

=>Sample(t1),Sample(t2),…,Sample(tn)

n=1,2,…

(14)

組合Vt,k(fi)的排序相當于DUV功能模型的順序性維度,代表了功能之間的切換。同時Sample(tn)是監控過程收集的結果,一個Seq可以混合Vt,k(fi)和子序列Seqsub,如式(15):

Seqt1,tn=Vt1,k(fi),Vt2,k(fi),…,Seqsub,…

(15)

原則上系統不停止,Seq可以是無限的。但是實際系統中,在序列Seq中具有相關性的Vt,k(fi)之間的跨度是有限的。如1-2相關,跨度為1,可表示Vt1,k(fi)和Vt2,k(fi)存在相關性。擴展順序性維度后,FCM的核心又擴展到序列Seq中組合Vt,k(fi)之間相關性的種類。

在一個實際的實現implementation中,一個變量uj可以通過一個或多個接口(interface)的相關序列Seq(intf)來表示,且滿足規則r(u,Seq(intf))。同樣,組合Vt,k(fi)和序列Seqt1,tn也可以根據規則r(V,Seq(intf))和r(Seq,Seq(intf))來通過和接口相關的序列Seq(intf)進行實現。

v(uj)=>Seqt1,tn(intfm),m=1,2,3,…n=1,2,3,…

r(u,Seq(intf))∈R(16)

Vt,k(fi)={v(uj)}=>{ Seqt1,tn(intfm)}

r(V,Seq(intf))∈R(17)

變量集合Sharedua_b表示b模塊的輸入變量且來源于a模塊的輸出變量,則有式(24)～式(26)。

DUV可以被看作是一個狀態機通過輸入觸發,其輸出函數僅由當前輸入或輸入和當前狀態決定。當前狀態又由初始狀態和輸入序列決定。在模塊化設計中,系統被分割成了很多模塊,系統功能集合Fsystem通過多模塊的協同工作實現,如式(27):

Fsystem=Fmodule_1×Fmodule_2×…×Fmodule_nn=1,2,3,…

(27)

模塊級驗證中模塊a的輸入直接被testbench控制。在系統級驗證中,testbench直接控制頂層輸入,此時模塊a的輸入被間接控制。對模塊a的間接控制通過頂層輸入和其他模塊,如式(28):

Fmodule_a=Fsystem/(Fmodule_1×Fmodule_2×…×Fmodule_n)n≠a

(28)

實際的模塊設計,特別是IP設計時,模塊的功能定義可能超出系統要求范圍或對模塊的原始功能需求描述,所以模塊a實現的功能集合Imp(Fmodule_a)可能會大于系統分配給該模塊的功能要求Ori(Fmodule_a):

Ori(Fmodule_a)?Imp(Fmodule_a)

(29)

在文獻[6]中,丟失的規格要求被發現來源于兩個連接模塊YοX中Y模塊的輸入域和X模塊的輸出域的失配。如果驗證Y通過控制X的輸入,那么對Y的驗證可能會存在一個漏洞。即相連的模塊X和模塊Y即使原始定義中沒有出現失配,但是在實現時也可能存在失配現象,表示為式(30)、式(31):

Domain_mis_o_i(Ori(Fmodule_X), Ori(Fmodule_Y))=φwhen SharedintfX_Y≠φ

(30)

◇?Domain_mis_o_i(Imp(Fmodule_X),Imp(Fmodule_Y))≠φwhen SharedintfX_Y≠φ

(31)

模塊驗證應該在系統驗證之前完成,但是即使如此,模塊功能也應該服務于系統需求,所以模塊間的失配并不一定是bug,可能是issue,這就意味著集成驗證或系統驗證時,模塊驗證組件的重用需要修改,比如覆蓋點。

但是如果原始分給a模塊的功能不在實現功能之中,或輸入輸出域不在實現之中,則必然存在bug,表示為

when Ori(Fmodule_a)￠Imp(Fmodule_a)or
Domain_i(Ori(Fmodule_a))￠ Domain_i(Imp(Fmodule_a))or Domain_o(Ori(Fmodule_a))￠ Domain_o(Imp(Fmodule_a)),□?a bug

(32)

2 測例層模型

由上述功能驗證的基本原理可知,不論使用何種語言進行驗證,不論使用何種驗證方法學或何種驗證組件構成的驗證環境,對功能的全面梳理最為重要。對于遵循標準協議的設計,功能驗證的重點是基于協議或規格,所以驗證組件的開發應該是一個梳理、理解、提取和轉換協議的過程。除了文字描述,協議還經常以波形圖、流程圖、狀態機圖、序列圖等表示。波形圖強調信號在時鐘周期級別的細節描述。流程圖聚焦于某一流程中面向不同中間結果的操作步驟。狀態機致力于其自身狀態轉換的描述。序列圖用于描述不同模塊之間的交互的場景。流程圖模型、狀態機圖模型、序列圖模型都屬于測例層的模型,以描述協議中的事務。同時類模型被用來記錄包結構和通用操作。協議中不好歸屬上述模型的,使用列表模型將其記錄,實現對協議的完全分解。自然語言描述存在隨意性和模糊性,形式語言描述對操作人員要求較高,測例層的模型是一種半形式化的方法適合理解和復查[7]。對協議進行列表化,將列表化后的協議向測例層模型進行映射,以檢查協議使用是否有疏漏,將測例層模型向代碼進行映射以檢查代碼中的漏洞,從而減少了人為引入的錯誤,并提高了代碼的協議可追溯性,如圖1所示。

映射過程需要量化協議,增加可數性。在協議中數據結構的量詞對應類和變量,描述操作的動詞轉化成任務和函數,對象的形容詞轉化成枚舉類型。通過分散的應用場景和通信場景聚合成一個完整的模型。不論全功能模型(FFMs)或總線功能模型(BFMs),功能模型應包括式(1)中功能集合F所涉及的所有功能,如圖2所示。

圖1 相關性映射

圖2 分散場景聚合為完整模型

圖3 驗證組件的同源性

激勵產生器、功能模型、覆蓋率收集是同源的,如圖3所示,它們是對協議特征的不同種表述形式。協議被列表化和模型化以后,屬性和斷言的提取變得更簡單,特別對于BFMs模型。類似圖形化的語言[8],模型提供了一個通過模板自動轉化為所需描述語言的機會,同時圖形化的模型便于分析[9]、評估[10]和遍歷[11]。由于功能與實現的分離,測例層的模型在作為一種黑盒方法應用時,可以面向滿足相同協議的任何設計?；跍y例層模型的driver可以通過算法遍歷模型中的所有需要的路徑,以重建測點和覆蓋率,從而彌補原始協議中可能未提出的盲點和缺陷。與形式化方法不同,其遍歷路徑后仍需要仿真驗證,針對的多為事務級處理對象,且可以根據需要遍歷具有特定特征的路徑。對于一個類模型,通過域的交錯來構建覆蓋點。對于一個流程圖模型,從起點到終點的所有路徑構成了各種測試場景。對于事務級狀態機模型,狀態的覆蓋點、狀態轉移的覆蓋點、狀態轉移序列的覆蓋點被建立。對于序列圖模型,所有多對象之間可能的通信可以被找到。這些都提高了驗證的完整性。功能模型作為一個可執行的協議,將通信和計算分離更適合重用、調試和性能評估。

不論是自頂向下還是自底向上的重用,不論是同一個設計不同階段的重用還是滿足同一個協議的不同設計之間的重用,對現存驗證資源的合理的調整方法是重用效率的保證。對于測例層模型的調整,使得代碼可以通過模板自動匹配模型而產生更改[12]。驗證技術管理中,對主特征,非主特征,邊角特征和不同優先級的劃分可以適應快速驗證和詳盡驗證的需求,這些需求可以在列表模型中實現。對于協議需要一個詳盡可配置的模型,再根據設計需求、不同的驗證級別和驗證組件,在該模型上進行選擇和定制化。在驗證的不同階段,模型需要不同的翻譯器和接口來針對不同抽象級別或不同接口協議之間進行轉換。對于局部特征的修改,通過修改模型中的節點來重新加入模型和重建組件,其復雜度和所修改模型節點的粒度相關,如圖4所示。

圖4 模型節點修改與重建

圖5 類模型構建讀寫器命令類及覆蓋率

3 GJB RFID的設計驗證

GJB RFID協議的工作頻率為840 MHz～845 MHz和920 MHz～925 MHz,頻帶內40個信道。讀寫器使用TPP基帶編碼,標簽使用FM0和Miller編碼。作為命令應答型系統,讀寫器和標簽都有啟動、初始化、處理命令、接收信號、傳送信號的過程。在事務級,接收和傳送命令的功能在編解碼之前。加解密功能需要鑒別。標簽的初始化流程導入參數來設置4個邏輯存儲區,信息區、編碼區、安全區和用戶區,預設各種標志位,比如滅活位、滅活使能位、鎖定使能位、安全模式。標簽類有3個狀態機模型,表述標簽狀態的轉換、FM0編碼和Miller編碼。前導碼與命令碼的處理過程分離。容差管理在接收和傳輸信號的過程中進行。讀寫器具有防碰撞DDS-BT機制,以及和上位機的通信。

讀寫器命令集分為盤點組命令和訪問組命令,包括分類命令(Sort)、啟動查詢命令(Query)、重復查詢命令(QueryRep)、分裂命令(Divide)、分散命令(Disperse)、收縮命令(Shrink)、編碼獲取命令(ACK)、應答錯誤命令(NAK)等。對命令的驗證使用約束性隨機驗證,并配合需要的場景。覆蓋率包括命令域值和交錯域,如圖5所示。

根據協議附錄B,可以構建出完整的標簽狀態機模型,并映射功能模型和覆蓋率,如圖6所示。流程圖模型在防碰撞機制的驗證,以及序列圖在安全鑒別協議的驗證中都有良好的驗證輔助效果。驗證平臺testbench基于UVM方法學及其組件,如圖7所示。根據測例層模型產生的testcase,通過調整testbench參數和握手接口,重用在了RFID驗證流程對標簽的驗證、對讀寫器的驗證以及它們內部的模塊驗證。Wrapper被用在了testbench與實現之間不同的通信需求上,比如取代接口、事務與信號的轉換、增加配置階段等。

圖6 狀態機模型構建標簽狀態轉換的功能和覆蓋率

圖7 測例層模型與UVM結合的驗證環境

最終通過測例層模型與UVM方法的配合,保證了GJB協議芯片的驗證覆蓋率,在TSMC0.18μm工藝流片,并測試成功,如圖8所示,為該類芯片的進一步改進和相關協議如ISO18000-6C協議芯片的開發積攢了大量可重用驗證組件,特別是與testcase層相關的組件。

圖8 流片與測試

4 結論與展望

本文通過詳細分析功能驗證的基本原理,同時基于近年來功能驗證在testbench可重用性上的發展情況,以及面向更多緯度上的重用性要求,提出了基于測例層模型的驗證。測例層模型是針對testcase層面建立的通用模型,包括類模型、列表模型、流程圖模型、狀態機圖模型、序列圖模型等,在實際應用中,根據具體的協議內容進行建模和填充,之后可以用于功能驗證的各個階段,形成了基于協議的測例級VIP。以UVM方法及其組件搭建驗證環境架構,將模型內容映射到驗證環境中進行功能驗證。以可數性、可追溯性的方式詮釋功能驗證的完整性。并以GJB RFID的設計驗證為例進行了說明。本文提出了較為通用的測例層模型,在實際應用中,面向特定結構或需求的驗證,比如cache一致性的驗證等,仍然可以在測例層探討更多的模型,以實現更廣范圍的驗證可重用性。

[1] Marella S K,Trivedi A R,Mukhopadhyay S.Optimization of FinFET-Based Circuits Using a Dual Gate Pitch Technique[C]//2015 IEEE/ACM International Conference on Computer-Aided Design(ICCAD),Austin,TX,2015:758-763.

[2] Clevenger L. Technology and Design Architectures and Process Innovations for 7 and 5 nm BEOL Interconnects[C]//2016 IEEE International Interconnect Technology Conference/Advanced Metallization Conference(IITC/AMC),San Jose,CA,2016:11-11.

[3] Chitti S,Chandrasekhar P,Asharani M. Ethernet MAC Verification by Efficient Verification Methodology for SOC Performance Improvement[C]//Proceedings of 3rd International Conference on Advanced Computing,Networking and Informatics,ICACNI 2015,Volume 2:117-123.

[4] Drechsler R,Chevallaz C,Fummi F. Panel:Future SoC Verification Methodology:UVM Evolution or Revolution[C]//2014 Design,Automation and Test in Europe Conference and Exhibition(DATE),Dresden,2014:1-5.

[5] Nahtigal T,Puhar P,?emva A. A Systematic Approach to Configurable Functional Verification of HW IP Blocks at Transaction Level[J]. Computers and Electrical Engineering,2012,38(6):1513-1523.

[6] Rodrigues C L,Silva K R G D,Cunha H N. Enhancing IP Cores Specifications Using Hierarchical Composition and Set Theory[J]. Des Autom Embed Syst,2011,15(3):225-245.

[7] Xie Z,Wang X A,Lian Z B. A Novel Intelligent Verification Platform Based on a Structured Analysis Model[J]. Sci China Inf Sci,2013,56(6):1-14.

[8] Zhar N,Ali M A,Eleuldj M,et al. VIP DESIGN:Graphical Language for Image and Video Processing Embedded Systems Design[C]//2012 International Conference on Complex Systems(ICCS),2012,229(5):1-6.

[9] Huzurbazar A V. Flowgraph Models:A Bayesian Case Study in Construction Engineering[J]. Journal of Statistical Planning and Inference,2005,129(s 1-2):181-193.

[10] Tan A T,Zainol Z,Budiarto R. Flowgraph Models for Estimating Total Time of Authentication Process in RFID System[J]. Journal of the Franklin Institute,2013,350(5):1298-1311.

[11] Li Q P,Xie Z,Su J T. UVM-Based Intelligent Verification Method for UHF RFID Tag[C]//2014 IEEE International Conference on Electron Devices and Solid-State Circuits(EDSSC),Chengdu,2014:1-2.

[12] Xie Z,Wang X A,Lian Z B. A Novel Reuse Technology of Extended Finite State Machine at the Transaction Level Based on UVM[J]. Advances in Electrical and Electronics Engineering,2014:305-314.

AFunctionVerificationMethodBasedontheModelsatTestCaseLevel*

XIEZheng1,WANGMingjiang1*,YONGShanshan2,WANGXin’an2

(1.Shenzhen Graduate School,Harbin Institute of Technology,Shenzhen Guangdong 518055,China;2.Peking University Shenzhen Graduate School,Shenzhen Guangdong 518055,China)

Aiming at the completeness and reusability in the integrated circuit function verification,the models at the test case level are proposed to build a protocol-oriented verification plan with complete functional coverage.The models cooperate with a verification environment built by UVM method and UVM library for an 800/900 MHz RFID system complied with GJB protocol. The models at test case level have generality. The models filled with protocol content meet the reusability between designs complied with the same protocol and the reusability between similar or nonholonomic protocols. That is a protocol-oriented VIP at the test case level and its construction method. Finally the models guarantee the verification coverage of the GJB protocol chip to tape out successfully in TSMC 0.18 μm.

function verification;model at test case level;RFID;UVM

10.3969/j.issn.1005-9490.2017.05.001

項目來源:深圳市科技計劃基礎研究項目(JCYJ20150403161923540)

2016-08-24修改日期2016-11-21

TN47

A

1005-9490(2017)05-1053-07

謝崢(1985-),男,漢族,山東人,哈爾濱工業大學深圳研究生院博士后,主要研究方向為集成電路設計驗證與智能硬件,xiezhengde@126.com;

王明江(1968-),男,漢族,黑龍江人,哈爾濱工業大學深圳研究生院教授,主要研究方向為集成電路與音視頻嵌入式系統研究,mjwang@hit.edu.cn。