吳 軍，華更新，劉鴻瑾

(北京控制工程研究所，北京100190)

SoC驗證方法學研究與應用

吳 軍，華更新，劉鴻瑾

(北京控制工程研究所，北京100190)

SoC系統(tǒng)功能日益復雜，規(guī)模也日益龐大，SoC驗證面臨著前所未有的挑戰(zhàn).對SoC驗證方法學進行了研究和總結，包括驗證流程、驗證層次和驗證技術.通過對基于DW 8051的SoC的驗證實踐，證明了這套驗證方法學的可行性和有效性.

SoC;驗證方法學;驗證流程;驗證層次;驗證技術

目前SoC的研究和應用已經(jīng)成為嵌入式計算機進一步發(fā)展的重要推動手段，其依托的原動力來自于半導體工藝的長足進步.隨著設計復雜度的不斷增大，驗證變得越來越困難.目前的SoC開發(fā)隊伍中，驗證人員一般是設計人員的2～3倍，驗證所花的時間和精力已占整個開發(fā)過程80%，驗證已經(jīng)成為整個SoC開發(fā)過程的瓶頸.本項目通過對SoC的驗證進行了方法的總結和歸納，在此基礎上利用對基于DW 8051微控制器的SoC的進行實踐來檢驗總結和歸納的方法的正確性和有效性，目的是掌握SoC的驗證體系，形成一套可信的驗證流程.

SoC的運算核心基于Synopsys?DW 8051 IP，在此基礎上增加了多種星敏感器的外圍接口邏輯.它具有以下的特點以及相對基本的8051微控制器的增強特性[1]:

(1)兼容工業(yè)標準的803x/805x

1)標準的8051指令集;

2)參數(shù)可選的全雙工串口;

3)3個Timer;

(2)高速體系結構

1)每個指令周期為4個時鐘周期;

2)指令執(zhí)行時間相比標準的8051可以有平均2.5倍的提高;

3)雙數(shù)據(jù)指針.

1 驗證方法學[2-6]

驗證與測試的區(qū)別首先需要明確，因為在實踐中往往存在有意混淆的傾向.在嵌入式軟件開發(fā)過程中，由于技術手段的原因，往往會不太刻意去區(qū)分測試(testing)與驗證(verification)，雖然兩者之間的區(qū)別原理上也是存在的，但是SoC本身是一個軟件和硬件的混合體，本質(zhì)是用軟件實現(xiàn)了一個硬件，從最終的產(chǎn)品形態(tài)上和傳統(tǒng)的ASIC并無差異，從來沒有任何理論會認為開發(fā)ASIC的過程是在開發(fā)一個軟件.SoC的開發(fā)過程存在采用EDA軟件與板級硬件兩種環(huán)境，實踐中大量存在利用測試代替驗證、重測試輕驗證等不正確的做法(測試速度快，相對容易，但可控性差，很難達到高覆蓋率)，所以必須嚴格區(qū)分.

測試的目的是去考察設計是否被正確“制造”出來，而驗證是為了確保這個設計能夠滿足需求規(guī)格說明所定義的功能和時序.圖1描述了測試與驗證之間的關系.簡單來說，在EDA軟件環(huán)境下叫做驗證，硬件實現(xiàn)后叫做測試.由于EDA軟件的特性，驗證可控性高，可以做到高覆蓋率，同時在EDA環(huán)境下所有的功能和時序特性和硬件測試完全一致，這是和傳統(tǒng)嵌入式軟件測試的最大不同，也是最大的優(yōu)點.

圖1 測試與驗證之間的關系Fig.1 Relationship between test and verification

驗證計劃是整個驗證的起點，它體現(xiàn)了驗證方法學的各個層面.作為整個驗證的需求規(guī)格說明，它來源于設計的規(guī)格說明.設計的規(guī)格說明相當于是驗證計劃的標準參考模型(golden reference).在驗證計劃中，需要明確以下幾個方面，同時也是驗證計劃中必須包括的項目:

1)驗證流程; 2)驗證目標; 3)驗證層次; 4)驗證技術.

1.1 驗證流程

驗證流程除了要說明驗證的計劃流程之外，還要明確驗證的技術流程.計劃流程是時間為出發(fā)點安排項目的各個節(jié)點，技術流程是安排從需求規(guī)格說明到項目目標所進行的驗證過程.計劃流程依照一般的工程節(jié)點管理即可.圖2是目前的從傳統(tǒng)集成電路實現(xiàn)流程引申而來的簡化SoC開發(fā)技術流程，其中包含了驗證工作.

1.2 驗證目標

驗證往往被認為是永無止境的任務，所以驗證計劃必須提供整個驗證流程成功的標志，也就是驗證的終點.一旦這個標志被確定，才能夠知道有多少驗證用例需要被生成，它們的復雜度以及依賴關系.譬如:一旦RTL通過了所有的驗證用例，而且對于覆蓋率和故障率達到預先定義的滿意值，則這個設計可以被通過了，而不是永無休止的驗證.這就是明確驗證目標所要達到的目的.

圖2 包含驗證的簡化SoC開發(fā)技術流程Fig.2 Simplified SoC design flow with verification

在實際工程中，如果想要一次成功，必須定義在什么樣的環(huán)境下，什么特點必須被執(zhí)行到，同時會有什么樣的期望反應.驗證計劃必須定義什么特點是必須被優(yōu)先驗證，什么特點是可選擇被驗證的.在驗證時間流程的壓力下，可能會故意從必須一次成功的點中放棄某些驗證點，當然這樣作必須經(jīng)過充分的評審.所以在驗證目標中需要明確定義以下幾點:

(1)功能點提取

這也是驗證目標中最難也是最精華部分.傳統(tǒng)的做法是從設計說明書中提取功能點，用自然語言來描述.理想的狀況是由設計工程師和驗證工程師來共同完成，設計工程師在設計階段就用文檔的形式定義所設計的模塊有哪些需要被驗證，這對于提高驗證的完整性有很大幫助，例如對于邊界用例(Corner case)的驗證就會有很大的幫助.最終，這些功能點由驗證工程師將其由自然語言轉(zhuǎn)換為驗證用例或形式化的斷言.本文將以舉例的方式詳細介紹基于DW 8051的SoC功能點的提取和描述方式.

(2)功能點響應

也就是正常工作狀態(tài)下，在相應激勵下的狀態(tài).

(3)功能點優(yōu)先級

定義哪些功能點必須被驗證，哪些是可選擇完成的.

(4)驗證結束標志

也就是讓設計被驗證通過的滿意值.例如代碼覆蓋率和功能覆蓋率分別需要達到的指標，通常代碼覆蓋率和功能覆蓋率要求達到80%～90%，更高的指標往往會增加數(shù)倍的工作量.

1.3 驗證層次

當準備一個驗證計劃時，需要解決的一個重要問題是要定義被驗證設計的粒度和層次.一個設計會隱含地包括幾個層次.一些設計會有一個物理分區(qū)，例如整個電路板.另外的設計會有一個邏輯分區(qū)，例如可綜合的單元和塊、可重用的 IP核或子系統(tǒng).如圖3所示.每一層的粒度僅僅只會最適合某一個特定的驗證目標.更小的分區(qū)更容易被驗證，因為它們提供更好的可控性和可觀察性.比起一個SoC芯片，在單元級更容易設計環(huán)境和狀態(tài)組合，更容易觀察是否響應為所期望的.如果更大的分區(qū)能夠被充分地驗證，其中包含的更小分區(qū)的完整性是默認地被驗證的，當然這是以更差的可控性和可觀測性為代價.對于驗證層次的規(guī)劃，在驗證計劃中有以下三點需要注意.

(1)分區(qū)劃分

任何待驗證的分區(qū)都必須要有相對穩(wěn)定的接口和實際意義的功能.如果接口一直在變化或者功能從一個分區(qū)移到另一個分區(qū)，那么驗證用例將不得不隨之改變，從而影響驗證進度.一旦已經(jīng)決定了某一個待驗證的特定分區(qū)，它們之間的接口和整個功能必須被盡早定義以及盡可能保持穩(wěn)定.理論上，每一個待驗證的分區(qū)應該有各自的說明文檔，或者至少在整個規(guī)格說明中有自己獨立一節(jié)來說明.

(2)單元驗證

與傳統(tǒng)的嵌入式軟件的單元不同，使用硬件描述語言描述的單元往往規(guī)模相對較小，一般也不具備有可獨立出來的完整功能.而且它們通常也沒有一個驗證所需要的獨立的規(guī)格說明.一般來說，單元驗證需要特定的驗證過程.設計者自己通過提供嵌入單元的斷言或在臨時的驗證平臺上，來驗證單元的基本操作.驗證的目標僅僅是去保證在RTL代碼中沒有語義錯誤，以及被操作的基本功能.它并不是為了去建立一個可收斂的驗證平臺以及得到很高的代碼覆蓋率.過多的設計單元會使驗證過程在單元級耗費太多的時間.每一個單元往往都會需要專門的驗證環(huán)境，完全沒有可移植性，寶貴的驗證資源往往耗費不正常的時間，只是為了一直都在變化的接口而去生成激勵生成器和響應監(jiān)視器.所以通常在SoC驗證層次規(guī)劃中，單純而且大量的單元驗證是沒有必要的，花費大量的時間去寫大量的簡單驗證用例還不如少一些但更復雜的驗證用例.其實在更高一級的子系統(tǒng)中，仍然會需要去驗證這些設計單元的完整性.原則上只推薦對一些非常復雜的單元去作專門的驗證.

圖3 驗證層次[6]Fig.3 Verification hierarchy

(3)驗證層次

和設計分區(qū)是緊密相關的，驗證的重點到底應該放在那一層，到底是單元級、模塊級或者是(子)系統(tǒng)級，這是驗證計劃需要明確的.目前的驗證理論強調(diào)模塊級應該是整個驗證的重點.模塊是由一些單元組成，驗證構架需要確保模塊級的驗證盡可能地充分，如果能夠保證模塊的功能得到充分驗證，其實它內(nèi)部所包含的子單元的完整性也會被同時得到充分驗證，而不需要去單獨驗證.這種觀點僅僅適用于采用硬件描述語言實現(xiàn)的設計，對于嵌入式軟件不一定適用.同時這樣作還會有兩個優(yōu)點:首先是這樣的構架容易建立可裁減和可重用的驗證平臺;另一點是能夠提高驗證的效率和產(chǎn)出.

1.4 驗證技術

對于驗證的結構以及在這個結構內(nèi)采用哪些驗證技術，其實這也是屬于驗證方法學的范疇.隨著SoC設計復雜度的不斷提高和設計規(guī)模的不斷增大，高效的驗證技術是提高驗證驗證完整性、效率和產(chǎn)出的重要因素.目前SoC驗證技術可以分為兩大類:基于仿真的驗證和基于形式化方法的驗證.在基于DW8051的SoC的驗證中，同時采用了仿真驗證和形式化驗證.

1.4.1 仿真驗證

基于仿真的，以覆蓋率作為驅(qū)動的驗證模型，是目前SoC驗證的流行驗證技術，基于DW8051的SoC的驗證就是建立在這個模型之上的.在這個模型內(nèi)，具體采用了覆蓋率驅(qū)動的驗證策略，一般以功能覆蓋率(functional coverage)目標作為驅(qū)動，代碼覆蓋率(code coverage)僅僅作為參考.通常來說，覆蓋率是被作為可信度建立的標準.它被用作為一個安全網(wǎng)絡去確保整個驗證計劃的完整性，同時也確保設計被盡可能的全面驗證.當大量的驗證用例完成后，覆蓋率的測量用來指明整個驗證過程的終點.

在基于DW 8051的SOC的驗證過程中，使用了基于分層結構的驗證方法學，通過將驗證平臺分成功能不同的幾個層面，增強了驗證平臺的封裝性和結構性.此外，引入面向?qū)ο篁炞C編程語言(system verilog)，可以極大的提高驗證工程師的驗證能力.如圖4中所示.驗證用例被運行在整個分層驗證環(huán)境的頂層.

圖4 驗證環(huán)境的分層結構Fig.4 Verification framework

1.4.1.1 層次結構

(1)信號層

這一層提供給驗證對象信號級的連接，在這里驗證對象是SoC設計.這一層提供給事件驅(qū)動信號名抽象以及連接.根據(jù)驗證環(huán)境的參考信號，這層也會抽象出信號的同步和時序.在基于 DW8051的SoC驗證中，驗證對象是使用Verilog實現(xiàn)的，驗證環(huán)境由System Verilog實現(xiàn)，信號層僅僅只包括System Verilog接口聲明.System Verilog接口還定義了信號同步(時鐘采樣)和時序(建立與保持)時間.驗證環(huán)境使用虛擬信號名而不是實際(通常是仿真器特定的)信號名.這樣允許驗證對象中信號和路徑(包括一些時鐘特性)改變后而不影響驗證環(huán)境和用例.

(2)命令層

命令層包含與出現(xiàn)在驗證對象中的不同接口和物理層協(xié)議關聯(lián)的總線功能模塊、物理層驅(qū)動和監(jiān)視器.它提供一個到驗證對象的固定的、底層的事務接口而不用去考慮驗證對象是怎樣被實現(xiàn)的.

(3)功能層

功能層提供必要的抽象層去處理應用級的事務和驗證驗證對象的正確性.不像以接口為基礎的物理層，功能事務是更高級操作的一個抽象.一個功能級的事務往往在不同的接口上需要執(zhí)行多個的命令層的事務.在整個運行時間里，根據(jù)具體的配置和激勵，比較器會自動去驗證驗證對象響應的正確性.具體到基于DW8051的SoC的驗證過程，比較器的輸入是運行程序的指針.同時在功能層，非常重要的事務是去收集功能覆蓋率，以此可以指導驗證用例的生成.運用了仿真器與System Verilog相互配合生成了一個覆蓋率模型，使用它記錄了所有事務處理過程中關于驗證對象的覆蓋率響應信息，可以很容易地做到功能覆蓋率的自動統(tǒng)計.

(4)場景層

這層提供了可控和可同步數(shù)據(jù)和事務生成器，它給驗證對象提供了很廣泛的激勵.不同的生成器被用于在功能層的不同子層提供數(shù)據(jù)和事務.本層也包括一個驗證對象的配置生成器.在基于DW8051的SoC驗證項目中，采用了隨機激勵生成器.

1.4.1.2 覆蓋率的指標

以覆蓋率作為驅(qū)動的驗證主要包含兩個含義:首先，可以通過覆蓋率指標來指導驗證工程師對驗證用例的生成;其次它可以明確驗證的終點.單純從覆蓋率的角度，在SoC驗證領域存在這四種覆蓋率指標:代碼覆蓋(code coverage)、功能覆蓋(functional coverage)、斷言覆蓋(asseration coverage)和形式化覆蓋(formal coverage).在實際工程中，基于DW 8051的SoC驗證中采用了代碼覆蓋率和功能覆蓋率指標作為驅(qū)動，在運行過程中收集整個覆蓋率信息.代碼覆蓋率高只是指明驗證用例遍歷了整個源代碼，而不能保證它的正確性和完整性.高的功能覆蓋率也并不意味著高的代碼覆蓋率.在基于DW 8051的SoC驗證過程中主要收集了以下一些覆蓋率信息.

(1)代碼覆蓋

1)語句覆蓋(Line coverage);

2)表達式覆蓋(Statement coverage);

3)區(qū)域覆蓋(Block coverage);

4)翻轉(zhuǎn)覆蓋(Toggle coverage);

5)狀態(tài)機覆蓋(FSM coverage);

6)條件覆蓋(Condition coverage);

7)分支覆蓋(Branch coverage);

8)路徑覆蓋(Path coverage).

(2)功能覆蓋

代碼覆蓋和功能覆蓋在表1和表4中有統(tǒng)計結果.

1.4.2 形式化驗證

形式化的驗證理論已有很多年的歷史，由于受到運算能力的限制在近幾年才開始被用戶采用.它主要包括:RTL規(guī)則檢查、等價性檢查和模型檢查.

對于以仿真為基礎的驗證，探索邊界用例的成功極大地依賴于驗證工程師的個人能力.首先，驗證工程師幾乎不可能考慮到所有驗證場景的組合可能，特別是在大型的設計里.其次，就算是有能力考慮到所有的邊界用例，也沒有足夠的時間去實現(xiàn).形式化驗證隱含遍歷整個狀態(tài)空間或子空間，這樣可以得到整個設計或部分設計的一個完整的驗證.然而，形式化驗證也不是一個萬能工具，他所達到的完整驗證取決于對設計特點表達的正確性.也就是說，形式化驗證不可能證明所有的特性都被驗證到.

1.4.2.1 形式化驗證和仿真驗證的比較

形式化驗證，對比于傳統(tǒng)的基于仿真的驗證，需要更多的數(shù)學背景去理解和有效的執(zhí)行.它們之間最顯著的區(qū)別是前者不需要輸入向量而后者需要.基于仿真的驗證過程首先是去生成輸入向量然后得到參考輸出.而形式化驗證過程正好相反.用戶開始先規(guī)定什么樣的行為是需要的然后讓形式化檢查器去證明.用戶根本就不需要去關心輸入激勵.從另一個方面來說，仿真驗證是由輸入驅(qū)動的，而形式化驗證是由輸出驅(qū)動的.通常輸入驅(qū)動的方式更加直接簡單，所以這也就說明形式化工具使用難度較大，由輸出來驅(qū)動驗證不太容易掌握.

仿真一個向量從概念上可以被認為是驗證了輸入空間的一個點.從這個觀點來看，仿真能夠被看作是輸入空間的采樣.除非所有的點都被采樣，否則存在一個錯誤被遺漏的可能.相對于在點一級工作，形式化驗證工作在特性一級.給定一個特性，形式化驗證工具會去遍歷所有可能的或?qū)е洛e誤的輸入和狀態(tài)條件.如果從輸出的觀點來看，仿真驗證在一個時刻驗證一個點而形式化驗證驗證一組點(一組點組成一個特性).圖5指明了它們之間的區(qū)別.這也使得在一個時刻驗證一組點讓形式化驗證不那么直接和容易使用.

圖5 從輸出空間的角度比較仿真驗證和形式化驗證Fig.5 Comparison between simulation verification and formal verification as viewed from out space

形式化驗證的主要缺點是在驗證目標到達之前需要大量的內(nèi)存和非常長的運行時間.當內(nèi)存容量被超過時，形式化工具經(jīng)常會屏蔽一些錯誤，或者只給用戶很少的指導去修復錯誤.所以，一般的形式化驗證只能夠被用來去遍歷中等大小的模塊.

1.4.2.2 規(guī)則檢查

在形式化驗證中，應用了規(guī)則檢查對源代碼進行了潛在危險的分析和模型檢查.一般的RTL規(guī)則檢查是根據(jù)不同的編程標準和設計規(guī)則，由預先定義的規(guī)則包去檢查用戶HDL設計.使用規(guī)則檢查的優(yōu)點在于它有異常嚴格的檢查規(guī)則，如果程序的確存在問題，幾乎不可能通過規(guī)則檢查.當然它的局限性在于它只能發(fā)現(xiàn)一些靜態(tài)錯誤，無法發(fā)現(xiàn)算法和數(shù)據(jù)流的錯誤.另一個局限性在于它用絕對懷疑的態(tài)度去報告分析的結果，它會盡量去報告所有可能的問題，所以造成報告出大量可能根本不存在的問題，需要用戶從大量的警告和錯誤報告中去篩選出真正的錯誤.

1.4.2.3 模型檢查

模型檢查被認為是最符合形式化的驗證技術.模型檢查器可以證明關于設計的一個特性或者斷言是真或者假.一般來說，使用這個工具有兩個用途:一個是用于驗證這個設計的某個特定部分，另一個是用來查找一些用戶無法想到或者無法用仿真來發(fā)現(xiàn)的錯誤.用戶可以使用這些形式化的工具來增強驗證.在本項目中，使用了模型檢查器對Timer模塊進行了功能驗證.目前驗證并且通過的功能:停止、啟動和加計數(shù).同時還對ALU模塊進行了驗證.

2 基于DW 8051的SoC驗證

對于基于DW 8051的SoC驗證是為了證明總結的驗證方法和流程的有效性，不是本文的重點，所以簡略介紹.基于DW8051的SoC的驗證流程如圖6所示，它也是由圖2中簡化的SoC開發(fā)技術流程通過研究和總結得到的.

圖6 基于DW 8051的SOC驗證流程Fig.6 DW8051-based SoC verification flow

以驗證覆蓋率為例，總共收集了以下覆蓋率指標作為驗證的驅(qū)動.

2.1 代碼覆蓋

其中語句覆蓋的結果舉例如表1所示.對于未能覆蓋的代碼均有分析.

2.2 功能覆蓋

在本項目中，對功能點的提取和功能覆蓋率的驗證方法進行了定義，下面舉例說明功能點的自然語言描述方法和功能覆蓋率的驗證方法和結果. 2.2.1 功能點的描述方法

關于指令級這項功能點的自然語言描述如表2所示，表2精確的描述了功能點在設計中發(fā)生的時間、位置和期望狀態(tài)，其他對功能點的描述可以此為標準.

表1 語句覆蓋Tab.1 Code coverage

表2 功能點的自然語言描述方法Tab.2 Description of function requirements by nature language

表3精確的描述了中具體到某一個指令的功能點的自然語言描述.

2.2.2 功能覆蓋的實現(xiàn)和結果

(1)驗證方法

使用了System Verilog實現(xiàn)上述這兩個用自然語言描述的功能點，仿真器會根據(jù)System Verilog的定義自動得到功能覆蓋率值.

(2)驗證結果(見表4)

表3 功能點的自然語言描述舉例Tab.3 Example of how to use nature language to describe function requirements

表4 功能覆蓋率的簡單描述Tab.4 Example of function coverage

3 驗證總結

通過對基于DW8051的SoC的驗證工作，從方法學的角度建立了一個完整的驗證系統(tǒng).在這樣一個系統(tǒng)內(nèi)，可以清晰地知道驗證的具體目標和構架，以及在驗證過程中，如何根據(jù)驗證目標的不同去有選擇的采取不同的驗證技術，同時還將不同驗證技術的適用范圍做了一個清晰的定義.

本文總結的驗證方法和流程，在隨后承擔的建立FPGA產(chǎn)品第三方驗證體系的前期籌劃工作中，為國內(nèi)首次實現(xiàn)的FPGA產(chǎn)品第三方驗證流程的制定打下了堅實基礎.

[1] Janick B.W riting testbenches:functional verification of HDL models[M].New York:Kluwer Academic Publishes，2003

[2] Andrew P.Functional verification coveragemeasurement and analysis[M].New York:K luwer Academic Publishers，2004

[3] Paul W.Professional verification:a guide to advanced functional verification[M].New York:Kluwer Academic Publishers，2004

[4] Janick B，Eduard Cerny，Alan H，et al.Verification methodology manual for system Verilog[M].New York: Springer Science Business Media，2005

[5] Janick B，W riting testbenches using system verilog [M].New York:Springer Science Business Media，2005

[6] W illiam K L.Hardware design verification:simulation and formal method-based approaches[M].Upper Sodd le River，New Jersey:Prentic-Hall，2005

Verification M ethodology Research and App lication for SoC

WU Jun，HUA Gengxin，LIU Hongjin
(Beijing Institute of Control Engineering，Beijing 100190，China)

The explosion of scale and comp lexity of SoC is currently becom ing a challenge for the SoC verification.The methodology illustrated in this paper is established based on the practice of DW 8051 SoC verification and its suitability and validity has been proved.This methodology includes verification flow，verification level and verification technique.

SoC;verification methodology;verification flow;verification level;verification technique

V249

A

1674-1579(2012)05-0027-07

10.3969/j.issn.1674-1579.2012.05.005

吳 軍(1976—)，男，高級工程師，研究方向為SoC驗證，容錯技術，嵌入式計算機;華更新(1965—)，男，研究員，研究方向為星載計算機體系結構設計;劉鴻瑾(1980—)，男，高級工程師，研究方向為星載計算機設計、SoC設計、抗輻射加固設計.

2012-02-10