SoC驗(yàn)證方法學(xué)研究與應(yīng)用

吳 軍，華更新，劉鴻瑾

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

SoC驗(yàn)證方法學(xué)研究與應(yīng)用

吳 軍，華更新，劉鴻瑾

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

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

SoC;驗(yàn)證方法學(xué);驗(yàn)證流程;驗(yàn)證層次;驗(yàn)證技術(shù)

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

SoC的運(yùn)算核心基于Synopsys?DW 8051 IP，在此基礎(chǔ)上增加了多種星敏感器的外圍接口邏輯.它具有以下的特點(diǎn)以及相對(duì)基本的8051微控制器的增強(qiáng)特性[1]:

(1)兼容工業(yè)標(biāo)準(zhǔn)的803x/805x

1)標(biāo)準(zhǔn)的8051指令集;

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

3)3個(gè)Timer;

(2)高速體系結(jié)構(gòu)

1)每個(gè)指令周期為4個(gè)時(shí)鐘周期;

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

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

1 驗(yàn)證方法學(xué)[2-6]

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

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

圖1 測(cè)試與驗(yàn)證之間的關(guān)系Fig.1 Relationship between test and verification

驗(yàn)證計(jì)劃是整個(gè)驗(yàn)證的起點(diǎn)，它體現(xiàn)了驗(yàn)證方法學(xué)的各個(gè)層面.作為整個(gè)驗(yàn)證的需求規(guī)格說(shuō)明，它來(lái)源于設(shè)計(jì)的規(guī)格說(shuō)明.設(shè)計(jì)的規(guī)格說(shuō)明相當(dāng)于是驗(yàn)證計(jì)劃的標(biāo)準(zhǔn)參考模型(golden reference).在驗(yàn)證計(jì)劃中，需要明確以下幾個(gè)方面，同時(shí)也是驗(yàn)證計(jì)劃中必須包括的項(xiàng)目:

1)驗(yàn)證流程; 2)驗(yàn)證目標(biāo); 3)驗(yàn)證層次; 4)驗(yàn)證技術(shù).

1.1 驗(yàn)證流程

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

1.2 驗(yàn)證目標(biāo)

驗(yàn)證往往被認(rèn)為是永無(wú)止境的任務(wù)，所以驗(yàn)證計(jì)劃必須提供整個(gè)驗(yàn)證流程成功的標(biāo)志，也就是驗(yàn)證的終點(diǎn).一旦這個(gè)標(biāo)志被確定，才能夠知道有多少驗(yàn)證用例需要被生成，它們的復(fù)雜度以及依賴關(guān)系.譬如:一旦RTL通過(guò)了所有的驗(yàn)證用例，而且對(duì)于覆蓋率和故障率達(dá)到預(yù)先定義的滿意值，則這個(gè)設(shè)計(jì)可以被通過(guò)了，而不是永無(wú)休止的驗(yàn)證.這就是明確驗(yàn)證目標(biāo)所要達(dá)到的目的.

圖2 包含驗(yàn)證的簡(jiǎn)化SoC開發(fā)技術(shù)流程Fig.2 Simplified SoC design flow with verification

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

(1)功能點(diǎn)提取

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

(2)功能點(diǎn)響應(yīng)

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

(3)功能點(diǎn)優(yōu)先級(jí)

定義哪些功能點(diǎn)必須被驗(yàn)證，哪些是可選擇完成的.

(4)驗(yàn)證結(jié)束標(biāo)志

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

1.3 驗(yàn)證層次

當(dāng)準(zhǔn)備一個(gè)驗(yàn)證計(jì)劃時(shí)，需要解決的一個(gè)重要問(wèn)題是要定義被驗(yàn)證設(shè)計(jì)的粒度和層次.一個(gè)設(shè)計(jì)會(huì)隱含地包括幾個(gè)層次.一些設(shè)計(jì)會(huì)有一個(gè)物理分區(qū)，例如整個(gè)電路板.另外的設(shè)計(jì)會(huì)有一個(gè)邏輯分區(qū)，例如可綜合的單元和塊、可重用的 IP核或子系統(tǒng).如圖3所示.每一層的粒度僅僅只會(huì)最適合某一個(gè)特定的驗(yàn)證目標(biāo).更小的分區(qū)更容易被驗(yàn)證，因?yàn)樗鼈兲峁└玫目煽匦院涂捎^察性.比起一個(gè)SoC芯片，在單元級(jí)更容易設(shè)計(jì)環(huán)境和狀態(tài)組合，更容易觀察是否響應(yīng)為所期望的.如果更大的分區(qū)能夠被充分地驗(yàn)證，其中包含的更小分區(qū)的完整性是默認(rèn)地被驗(yàn)證的，當(dāng)然這是以更差的可控性和可觀測(cè)性為代價(jià).對(duì)于驗(yàn)證層次的規(guī)劃，在驗(yàn)證計(jì)劃中有以下三點(diǎn)需要注意.

(1)分區(qū)劃分

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

(2)單元驗(yàn)證

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

圖3 驗(yàn)證層次[6]Fig.3 Verification hierarchy

(3)驗(yàn)證層次

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

1.4 驗(yàn)證技術(shù)

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

1.4.1 仿真驗(yàn)證

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

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

圖4 驗(yàn)證環(huán)境的分層結(jié)構(gòu)Fig.4 Verification framework

1.4.1.1 層次結(jié)構(gòu)

(1)信號(hào)層

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

(2)命令層

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

(3)功能層

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

(4)場(chǎng)景層

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

1.4.1.2 覆蓋率的指標(biāo)

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

(1)代碼覆蓋

1)語(yǔ)句覆蓋(Line coverage);

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

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

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

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

6)條件覆蓋(Condition coverage);

7)分支覆蓋(Branch coverage);

8)路徑覆蓋(Path coverage).

(2)功能覆蓋

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

1.4.2 形式化驗(yàn)證

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

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

1.4.2.1 形式化驗(yàn)證和仿真驗(yàn)證的比較

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

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

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

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

1.4.2.2 規(guī)則檢查

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

1.4.2.3 模型檢查

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

2 基于DW 8051的SoC驗(yàn)證

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

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

以驗(yàn)證覆蓋率為例，總共收集了以下覆蓋率指標(biāo)作為驗(yàn)證的驅(qū)動(dòng).

2.1 代碼覆蓋

其中語(yǔ)句覆蓋的結(jié)果舉例如表1所示.對(duì)于未能覆蓋的代碼均有分析.

2.2 功能覆蓋

在本項(xiàng)目中，對(duì)功能點(diǎn)的提取和功能覆蓋率的驗(yàn)證方法進(jìn)行了定義，下面舉例說(shuō)明功能點(diǎn)的自然語(yǔ)言描述方法和功能覆蓋率的驗(yàn)證方法和結(jié)果. 2.2.1 功能點(diǎn)的描述方法

關(guān)于指令級(jí)這項(xiàng)功能點(diǎn)的自然語(yǔ)言描述如表2所示，表2精確的描述了功能點(diǎn)在設(shè)計(jì)中發(fā)生的時(shí)間、位置和期望狀態(tài)，其他對(duì)功能點(diǎn)的描述可以此為標(biāo)準(zhǔn).

表1 語(yǔ)句覆蓋Tab.1 Code coverage

表2 功能點(diǎn)的自然語(yǔ)言描述方法Tab.2 Description of function requirements by nature language

表3精確的描述了中具體到某一個(gè)指令的功能點(diǎn)的自然語(yǔ)言描述.

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

(1)驗(yàn)證方法

使用了System Verilog實(shí)現(xiàn)上述這兩個(gè)用自然語(yǔ)言描述的功能點(diǎn)，仿真器會(huì)根據(jù)System Verilog的定義自動(dòng)得到功能覆蓋率值.

(2)驗(yàn)證結(jié)果(見表4)

表3 功能點(diǎn)的自然語(yǔ)言描述舉例Tab.3 Example of how to use nature language to describe function requirements

表4 功能覆蓋率的簡(jiǎn)單描述Tab.4 Example of function coverage

3 驗(yàn)證總結(jié)

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

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

[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—)，男，高級(jí)工程師，研究方向?yàn)镾oC驗(yàn)證，容錯(cuò)技術(shù)，嵌入式計(jì)算機(jī);華更新(1965—)，男，研究員，研究方向?yàn)樾禽d計(jì)算機(jī)體系結(jié)構(gòu)設(shè)計(jì);劉鴻瑾(1980—)，男，高級(jí)工程師，研究方向?yàn)樾禽d計(jì)算機(jī)設(shè)計(jì)、SoC設(shè)計(jì)、抗輻射加固設(shè)計(jì).

2012-02-10