Cache一致性驗(yàn)證的結(jié)構(gòu)化激勵(lì)生成算法

程開豐 羅漢青 梁利平

摘 要：為解決Cache一致性驗(yàn)證中傳統(tǒng)隨機(jī)激勵(lì)方法的冗余覆蓋及覆蓋死角等問題，提出了一種高層次結(jié)構(gòu)化激勵(lì)生成算法和相應(yīng)的高層次功能覆蓋率模型.首先根據(jù)實(shí)際多核應(yīng)用場(chǎng)景將沖突訪存操作分類成基本同步和復(fù)雜同步，并進(jìn)一步抽象成有向二分圖模型，由此提出一種通用的層次化輸入空間等價(jià)類劃分算法和對(duì)應(yīng)的高層次HSPC（Host Slave Pair Coverage）功能覆蓋率模型，最后基于樹的搜索提出了結(jié)構(gòu)化激勵(lì)生成算法.上述方案成功應(yīng)用于IMEDiamond SoC的Cache一致性的功能驗(yàn)證中，實(shí)際結(jié)果表明，相比傳統(tǒng)基于代碼的覆蓋率，高層次HSPC功能覆蓋率模型的揭示功能Bug能力更強(qiáng)，而且相對(duì)于傳統(tǒng)的隨機(jī)生成，結(jié)構(gòu)化的激勵(lì)能夠?qū)⒏采w率收斂所需的激勵(lì)數(shù)減少96.3%.

關(guān)鍵詞：Cache一致性；有向二分圖模型；等價(jià)類劃分；高層次功能覆蓋率模型；結(jié)構(gòu)化激勵(lì)生成

中圖分類號(hào)：TP302 文獻(xiàn)標(biāo)志碼：A

Abstract： In order to deal with the problems of redundant and failed coverage in the traditional random stimuli for cache coherence verification， a high level structural stimuli generation algorithm and the corresponding functional coverage model were presented. Firstly， conflict memory accesses were categorized into basic/complex synchronizations， and thus abstracted into general bipartite graph model. Consequently， a general layered equivalence partition algorithm of ISS and the corresponding high level HSPC （Host Slave Pair Coverage） functional coverage model were proposed. Finally， two structural stimuli generation algorithms based on the search of ISS tree were presented. Experiments were performed in the functional verification of the cache system of IMEDiamond SoC， and the result indicates the HSPC coverage model can help uncover functional bugs more easily when compared with code coverage， and structural stimuli generation can reduce 96.3% stimuli for coverage convergence when compared with random stimuli generation.

Key words：Cache coherence； directed bipartite graph model； equivalence partition； high level functional coverage model； structural stimuli generation

所有基于仿真的功能驗(yàn)證都需要做好兩個(gè)環(huán)節(jié)：輸入激勵(lì)的生成與最后結(jié)果正確性的判斷.Cache一致性的驗(yàn)證是多處理器系統(tǒng)功能驗(yàn)證中非常重要的一個(gè)部分.其輸入激勵(lì)是多核并行訪存程序，結(jié)果正確性的判斷是基于特定的內(nèi)存一致性模型（MCC，Memory Consistency Model）.

在已有的相關(guān)研究中，1979年Lamport[1]提出了順序一致性模型（Sequential Consistency， SC），由于SC模型最符合程序員的直觀思維，所以在多處理器系統(tǒng)設(shè)計(jì)和驗(yàn)證中一直占主導(dǎo)地位.1994年Gibbons和Korach[2]在理論上分析了存儲(chǔ)一致性驗(yàn)證的復(fù)雜性，其中把在SC模型下的驗(yàn)證定義為VSC（Verifying Sequential Consistency）問題，并證明了VSC是NP難問題.1997年胡偉武等[3]給出了另一種SC模型下判斷多核訪存操作正確性的方法.與Gibbons等只根據(jù)訪存結(jié)果來尋找判斷是否存在多核順序交織序列不同，該方法關(guān)注記錄了多核程序PRG的靜態(tài)程序PRO（PRG）和動(dòng)態(tài)執(zhí)行序E（PRG），并指出最后執(zhí)行結(jié)果符合SC的充要條件是E（PRG）SymbolHC@ PRO（PRG）對(duì)應(yīng)的有向圖無環(huán).上述研究本質(zhì)都是關(guān)于Cache一致性結(jié)果正確性判斷，缺少對(duì)輸入多核程序生成方法的研究.

1990年Wood等[4]采用了仿真的手段對(duì)多核一致性協(xié)議進(jìn)行了驗(yàn)證，其中多核訪存程序采用的是隨機(jī)生成.2010年王朋宇等[5]在文獻(xiàn)[3]的工作基礎(chǔ)上實(shí)現(xiàn)了一種線性時(shí)間復(fù)雜度的片上多核處理器存儲(chǔ)一致性驗(yàn)證工具LCHECK，其中多核訪存程序生成部分仍采用隨機(jī)的策略.可見現(xiàn)有對(duì)Cache一致性驗(yàn)證時(shí)的激勵(lì)基本都基于隨機(jī)生成，隨機(jī)化方法雖然有時(shí)能夠發(fā)現(xiàn)一些corner bug，但有兩個(gè)明顯的不足：

1）現(xiàn)實(shí)中輸入激勵(lì)空間（ISS，Input Stimuli Space）的元素并不是均勻分布的，而隨機(jī)產(chǎn)生輸入激勵(lì)時(shí)并不考慮此等情況，故最后對(duì)ISS的覆蓋是不均勻的，即簡單的激勵(lì)點(diǎn)會(huì)被反復(fù)覆蓋，而困難的激勵(lì)點(diǎn)則很難甚至無法覆蓋；

2）多核相對(duì)單核最大的特點(diǎn)是允許無沖突程序間的并行執(zhí)行，以提高整體性能，故絕大多數(shù)實(shí)際的多核應(yīng)用程序不會(huì)隨意進(jìn)行Cache一致性操作，而是在特定情形下有規(guī)律的進(jìn)行.隨機(jī)產(chǎn)生的多核程序也沒有考慮此實(shí)際情況，本文在考慮了實(shí)際的多核應(yīng)用特點(diǎn)下，針對(duì)Cache一致性的功能驗(yàn)證提出了一套通用的ISS高層次抽象和等價(jià)類劃分方法，并提出了高層次的HSPC（Host Slave Pair Coverage）功能覆蓋率模型以及基于樹遍歷的結(jié)構(gòu)化激勵(lì)生成算法，最后通過實(shí)際的工程檢驗(yàn)證明：相比傳統(tǒng)的基于RTL代碼的覆蓋率模型，HSPC功能覆蓋率模型能更好地幫助發(fā)現(xiàn)功能bug；相比傳統(tǒng)隨機(jī)生成驗(yàn)證激勵(lì)，同等覆蓋率下，結(jié)構(gòu)化激勵(lì)能夠大幅減少測(cè)試激勵(lì)數(shù)目，縮短驗(yàn)證周期.

1 具體方案

1.1 有向二分圖模型

在Cache一致性系統(tǒng)的仿真驗(yàn)證中，其輸入激勵(lì)為多核沖突訪存程序.由于多核相對(duì)單核最大的特點(diǎn)是允許無沖突程序間的并行執(zhí)行，以提高整體性能.故對(duì)實(shí)際的多核Cache一致性操作的應(yīng)用場(chǎng)景有如下基本假設(shè)：

A1）多核沖突訪存程序一般應(yīng)用于多核間特定節(jié)點(diǎn)的同步；

A2）多核同步可分為基本同步（Basic Synchronization，BS）與復(fù)雜同步（Complex Synchronization，CS），其中CS可以分解為多個(gè)BS操作；

A3）BS本質(zhì)上為單寫多讀（Single Write Multiple Read，SWMR）的多核沖突訪存程序，且要求BS中所有讀操作最后要能讀到BS中寫操作的值；

A4）同一CS中包含的各BS之間訪存地址不同；但對(duì)具體的訪存地址的值和數(shù)據(jù)不敏感.

A5）不同核之間可以區(qū)分，即不具有對(duì)稱性.

A6）有意義的程序中任何核的任何有意義的寫操作都會(huì)有至少一個(gè)讀操作與其對(duì)應(yīng).

上述假設(shè)是合理的，因?yàn)橐韵聝牲c(diǎn)：

1）基于snoopy的MESI等Cache一致性協(xié)議在設(shè)計(jì)時(shí)就并不關(guān)心絕對(duì)的訪存地址的值，而只關(guān)心多核訪存地址間是否沖突等相對(duì)關(guān)系.

2）多核系統(tǒng)中一般都會(huì)有主核與從核之分，而且不同核與snoopy等一致性模塊間的物理延時(shí)一般也是不同的，所以不同核之間是可以區(qū)分的.

由此可將多核CS操作抽象成有向二分圖模型（DBGM，Directed Bipartite Graph Model）G=〈Vw，Vr，E〉，其中圖的各元素含義如下.

1）主點(diǎn)集Vw：發(fā)起寫操作的內(nèi)核抽象成頂點(diǎn)后構(gòu)成的集合；

2）從點(diǎn)集Vr：發(fā)起讀操作的內(nèi)核抽象成頂點(diǎn)后構(gòu)成的集合；

3）點(diǎn)集V：所有參與訪存操作的內(nèi)核抽象成頂點(diǎn)后構(gòu)成的集合，即V=Vw∪Vr；

4）有向邊集E：Vw中頂點(diǎn)vwi到Vr中頂點(diǎn)vrj之間存在有向邊eij=〈vwi，vrj〉的充要條件是vri對(duì)應(yīng)內(nèi)核發(fā)起的讀操作的結(jié)果來自vwi對(duì)應(yīng)內(nèi)核發(fā)起的寫操作.

一個(gè)示例CS的有向二分圖模型如圖1所示.

1.4 結(jié)構(gòu)化激勵(lì)生成

結(jié)構(gòu)化激勵(lì)生成算法分成如下兩步：

步驟1：對(duì)ISST的葉子節(jié)點(diǎn)進(jìn)行搜索遍歷以確定SysSti中各活動(dòng)主從核及相應(yīng)的主從對(duì)應(yīng)關(guān)系；

步驟2：根據(jù)基本假設(shè)A4，SysSti中BS對(duì)具體訪存地址是不敏感的，故當(dāng)遍歷得到每個(gè)葉子節(jié)點(diǎn)后，既得到了Cache一致性驗(yàn)證激勵(lì)所需要的三大核心信息：活躍主核、活躍從核劃分以及主從之間的對(duì)應(yīng)關(guān)系，然后隨機(jī)產(chǎn)生訪存地址及訪存數(shù)據(jù)等細(xì)節(jié)信息以生成最終的激勵(lì).

上述激勵(lì)生成算法產(chǎn)生的激勵(lì)不僅保留了底層邏輯信號(hào)級(jí)隨機(jī)性，而且能在高層次上充分保證對(duì)ISS的高覆蓋率.

下面重點(diǎn)介紹第一步，即對(duì)ISS樹的搜索遍歷.在介紹具體的搜索算法之前，首先介紹一個(gè)重要的轉(zhuǎn)換關(guān)系.根據(jù)1.3節(jié)中的劃分算法，每個(gè)葉節(jié)點(diǎn)Si，j，k，l可以由其下標(biāo)四元組〈i，j，k，l〉來唯一索引確定，故葉子節(jié)點(diǎn)的搜索遍歷就轉(zhuǎn)換成了對(duì)〈i，j，k，l〉四元組的搜索遍歷.

由于經(jīng)典計(jì)算機(jī)算法中對(duì)樹的搜索有深度優(yōu)先搜索（DFS，Depth First Search）和寬度優(yōu)先搜索（BFS，Breadth First Search）兩大類，此處可以加以借鑒，但與經(jīng)典樹搜索需要遍歷所有節(jié)點(diǎn)不同的是，此ISS樹只需要搜索葉子節(jié)點(diǎn)，所以相應(yīng)的搜索算法在細(xì)節(jié)上也有些許不同，具體分別介紹如下.

1.4.1 DFS

其基本思想從激勵(lì)角度看是個(gè)嚴(yán)格的順序關(guān)系，每種特定的主接口組合要驅(qū)動(dòng)完所有可能的從接口，然后再切換到下一種主接口組合；而且對(duì)于主接口組合，先考慮單一主接口，然后是2個(gè)主接口同時(shí)發(fā)請(qǐng)求，再是3個(gè)主接口同時(shí)，一直到最后所有主接口同時(shí)發(fā)請(qǐng)求.從ISS樹角度看，第3層所有葉子節(jié)點(diǎn)按照從左到右的順序被遍歷，具體算法實(shí)現(xiàn)的流程如圖3所示.

其中NumChild（S）函數(shù)返回節(jié)點(diǎn)S的兒子節(jié)點(diǎn)數(shù)目.

1.4.2 BFS

其基本思想從激勵(lì)角度看是個(gè)循環(huán)關(guān)系，每個(gè)循環(huán)內(nèi)部每種特定的主接口組合驅(qū)動(dòng)完一種可能的從接口后就切換到另一主接口組合，直到所有的主接口組合都被遍歷到.從ISS樹角度看，S1，S2，…，SNHI的葉子節(jié)點(diǎn)交替地被遍歷，具體算法實(shí)現(xiàn)的流程如圖4所示.

其中CycInc（x）函數(shù)是對(duì)變量x進(jìn)行循環(huán)遞增（當(dāng)x超過最大值時(shí)，回歸到最小值）；Searched（S）函數(shù)返回1時(shí)，表示以S為根節(jié)點(diǎn)的子樹已經(jīng)被搜索，否則返回0；Dead（S）返回1時(shí)表示以S為根節(jié)點(diǎn)的子樹中所有葉子節(jié)點(diǎn)都已經(jīng)被遍歷，否則返回0.

2 驗(yàn)證實(shí)例

為具體展示上述激勵(lì)方案的效果，本文選擇了IMEDiamond系統(tǒng)作為功能驗(yàn)證實(shí)例.

為比較不同覆蓋率模型，幫助揭示Bug的能力，實(shí)驗(yàn)對(duì)比了Line、Condition和Toggle等基于代碼的覆蓋率和本文所提出的高層次HSPC功能覆蓋率，各覆蓋率值與揭示的功能bug數(shù)間關(guān)系.考慮到多核Cache訪問時(shí)，最主要的功能缺陷來自多核競(jìng)爭(zhēng)和異核交互（即多個(gè)核有寫操作以及一個(gè)核讀取另一核寫的值），所以實(shí)驗(yàn)時(shí)的bug模型也模擬了這種錯(cuò)誤，分別在多核競(jìng)爭(zhēng)和異核交互時(shí)引入缺陷（比如多個(gè)核有寫操作時(shí)仲裁錯(cuò)誤以及一個(gè)核讀取另一核寫的值時(shí)錯(cuò)誤）.最終的實(shí)驗(yàn)結(jié)果統(tǒng)計(jì)如圖5所示.

由圖 5可以有以下結(jié)論：

1）相對(duì)所有的代碼覆蓋率，HSPC都能夠在很小的覆蓋率下發(fā)現(xiàn)同樣數(shù)目的功能bug；

2）代碼覆蓋率很難達(dá)到100%，而HSPC卻能夠達(dá)到100%；

3）最終覆蓋率收斂時(shí)，HSPC指導(dǎo)下發(fā)現(xiàn)的功能bug數(shù)要多于代碼覆蓋率.綜上可見，HSPC揭示功能bug的能力比傳統(tǒng)的代碼覆蓋率要更強(qiáng)大.

為比較不同的激勵(lì)生成算法所產(chǎn)生激勵(lì)與功能覆蓋率之間的關(guān)系，實(shí)驗(yàn)比較了不同核數(shù)NC下為達(dá)到相同100% 的HSPC覆蓋率，本文結(jié)構(gòu)化方法所需激勵(lì)數(shù)StructStiNum相對(duì)傳統(tǒng)隨機(jī)方法所需激勵(lì)數(shù)RanStiNum減少的比例ReduceRatio=1-StructStiNumRanStiNum，如圖6所示.

由圖 6可見，隨著核數(shù)的增加，ReduceRatio一直呈上升趨勢(shì)，即隨機(jī)化方法產(chǎn)生的激勵(lì)中冗余激勵(lì)的比例越來越高.NC=8時(shí)，ReduceRatio已經(jīng)達(dá)到了96.3%.

此外在16核Intel Xeon E5520、主頻2.27 GHz、內(nèi)存25 GB、Linux系統(tǒng)環(huán)境下，LeafNum及激勵(lì)生成時(shí)間（StrucTsti為結(jié)構(gòu)化激勵(lì)時(shí)間，RanTsti為隨機(jī)激勵(lì)時(shí)間）與NC之間的關(guān)系統(tǒng)計(jì)如表1所示.

由表1可有以下結(jié)論：

1）激勵(lì)生成時(shí)間與LeafNum一樣，與NC之間都是指數(shù)增長關(guān)系，符合公式（2）.

2）在NC≤8時(shí)結(jié)構(gòu)化激勵(lì)生成時(shí)間最大也就44 s，而隨機(jī)激勵(lì)已經(jīng)到了3 883 s，是結(jié)構(gòu)化方法的87倍.

3）本文的方法適合核數(shù)NC不是很大的多核系統(tǒng)，當(dāng)NC超過8時(shí)，為了控制激勵(lì)生成時(shí)間，需要采取進(jìn)一步的輸入空間化簡方法.

3 結(jié) 語

為解決傳統(tǒng)多核處理器Cache一致性驗(yàn)證中隨機(jī)激勵(lì)方法的冗余覆蓋及傳統(tǒng)代碼覆蓋率模型揭錯(cuò)率低等問題，本文根據(jù)多核應(yīng)用程序本身的特點(diǎn)，提出了一種多核沖突訪存抽象建模的方法，并由此進(jìn)一步給出了相應(yīng)的高層次HSPC功能覆蓋率模型和結(jié)構(gòu)化激勵(lì)生成算法.實(shí)際系統(tǒng)的驗(yàn)證效果表明相比傳統(tǒng)的代碼覆蓋率，HSPC覆蓋率模型的揭示功能Bug的能力更強(qiáng)；而且相對(duì)于傳統(tǒng)的純隨機(jī)激勵(lì)，結(jié)構(gòu)化的激勵(lì)消除了冗余，能夠更快地加快覆蓋率收斂.

此外對(duì)于單核發(fā)起多個(gè)寫操作的情形，由于物理上不同的寫也是順序發(fā)起的，根據(jù)前述基本假設(shè)A6，每個(gè)寫都有各自對(duì)應(yīng)的讀操作，所以可以根據(jù)不同寫發(fā)起的時(shí)間先后，將不同的寫劃歸入不同的時(shí)間片，每個(gè)時(shí)間片內(nèi)每個(gè)核只有一個(gè)寫操作，此時(shí)本文的方法仍然適用.

參考文獻(xiàn)

[1] LAMPORT L. How to make a multiprocessor computer that correctly executes multiprocessor programs [J]. IEEE Transaction on Computers， 1979， C-28（9）： 690-691.

[2] GIBBONS P B，KORACH E. On testing cachecoherent shared memories [C]// ACM Symposium on Parallel Algorithms and Architectures. 1994： 177-188.

[3] 胡偉武，夏培肅. 順序一致共享存儲(chǔ)系統(tǒng)中的亂序執(zhí)行技術(shù)基本理論[J]. 計(jì)算機(jī)學(xué)報(bào)， 1997，20（6）： 481-490.

HU W W， XIA P S. Outoforder execution in sequentially consistent shared memory systems： principles[J]. Chinese Journal of Computers， 1997，20（6）： 481-490. （In Chinese）

[4] WOOD D A， GIBSON G A， AND KATZ R H. Verifying a multiprocessor cache controller using random test generation [J]. IEEE Design and Test， 1989， 7（4）：13-25.

[5] 王朋宇， 陳云霽，沈海華， 等. 片上多核處理器存儲(chǔ)一致性驗(yàn)證[J]. 軟件學(xué)報(bào)， 2010， 21（4）： 863-874.

WANG P Y， CHEN Y J， SHEN H H， et al. Memory consistency verification of chip multiprocessor[J]. Journal of Software， 2010， 21（4）： 863-874. （In Chinese）

[6] GRAHAM R L， KNUTH D E， PATASHNIK O.Concrete mathematics[M]. USA： AddisonWesley， 1994： 257-267.

[7] 王志君，梁利平，吳凱 ，等.一種面向多媒體和通信應(yīng)用的處理器指令集及架構(gòu)實(shí)現(xiàn)[J].湖南大學(xué)學(xué)報(bào)（自然科學(xué)版）， 2014，41（10）：108-114.

WANG Z J， LIANG L P， WU K， et al. Architecture and implementation of an application specific instruction set for multimedia and communication[J]. Journal of Hunan University（Natural Sciences）， 2014，41（10）：108-114. （In Chinese）

[8] 王志君，梁利平， 洪欽智 ，等.一種DSP和通用CPU一體化的處理器架構(gòu)及其4核實(shí)現(xiàn)[J].微電子學(xué)與計(jì)算機(jī)，2014，31（10）：32-38.

WANG Z J， LIANG L P， HONG Q Z， et al.The architecture of an unified DSP plus generalpurpose CPU and the implementation of a 4core homogenous processor[J]. Microelectronics & Computer， 2014，31（10）：32-38.（In Chinese）