Cache一致性驗證的結構化激勵生成算法

程開豐 羅漢青 梁利平

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

關鍵詞：Cache一致性；有向二分圖模型；等價類劃分；高層次功能覆蓋率模型；結構化激勵生成

中圖分類號：TP302 文獻標志碼：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

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

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

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

1）現實中輸入激勵空間（ISS，Input Stimuli Space）的元素并不是均勻分布的，而隨機產生輸入激勵時并不考慮此等情況，故最后對ISS的覆蓋是不均勻的，即簡單的激勵點會被反復覆蓋，而困難的激勵點則很難甚至無法覆蓋；

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

1 具體方案

1.1 有向二分圖模型

在Cache一致性系統的仿真驗證中，其輸入激勵為多核沖突訪存程序.由于多核相對單核最大的特點是允許無沖突程序間的并行執行，以提高整體性能.故對實際的多核Cache一致性操作的應用場景有如下基本假設：

A1）多核沖突訪存程序一般應用于多核間特定節點的同步；

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

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

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

A5）不同核之間可以區分，即不具有對稱性.

A6）有意義的程序中任何核的任何有意義的寫操作都會有至少一個讀操作與其對應.

上述假設是合理的，因為以下兩點：

1）基于snoopy的MESI等Cache一致性協議在設計時就并不關心絕對的訪存地址的值，而只關心多核訪存地址間是否沖突等相對關系.

2）多核系統中一般都會有主核與從核之分，而且不同核與snoopy等一致性模塊間的物理延時一般也是不同的，所以不同核之間是可以區分的.

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

1）主點集Vw：發起寫操作的內核抽象成頂點后構成的集合；

2）從點集Vr：發起讀操作的內核抽象成頂點后構成的集合；

3）點集V：所有參與訪存操作的內核抽象成頂點后構成的集合，即V=Vw∪Vr；

4）有向邊集E：Vw中頂點vwi到Vr中頂點vrj之間存在有向邊eij=〈vwi，vrj〉的充要條件是vri對應內核發起的讀操作的結果來自vwi對應內核發起的寫操作.

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

1.4 結構化激勵生成

結構化激勵生成算法分成如下兩步：

步驟1：對ISST的葉子節點進行搜索遍歷以確定SysSti中各活動主從核及相應的主從對應關系；

步驟2：根據基本假設A4，SysSti中BS對具體訪存地址是不敏感的，故當遍歷得到每個葉子節點后，既得到了Cache一致性驗證激勵所需要的三大核心信息：活躍主核、活躍從核劃分以及主從之間的對應關系，然后隨機產生訪存地址及訪存數據等細節信息以生成最終的激勵.

上述激勵生成算法產生的激勵不僅保留了底層邏輯信號級隨機性，而且能在高層次上充分保證對ISS的高覆蓋率.

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

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

1.4.1 DFS

其基本思想從激勵角度看是個嚴格的順序關系，每種特定的主接口組合要驅動完所有可能的從接口，然后再切換到下一種主接口組合；而且對于主接口組合，先考慮單一主接口，然后是2個主接口同時發請求，再是3個主接口同時，一直到最后所有主接口同時發請求.從ISS樹角度看，第3層所有葉子節點按照從左到右的順序被遍歷，具體算法實現的流程如圖3所示.

其中NumChild（S）函數返回節點S的兒子節點數目.

1.4.2 BFS

其基本思想從激勵角度看是個循環關系，每個循環內部每種特定的主接口組合驅動完一種可能的從接口后就切換到另一主接口組合，直到所有的主接口組合都被遍歷到.從ISS樹角度看，S1，S2，…，SNHI的葉子節點交替地被遍歷，具體算法實現的流程如圖4所示.

其中CycInc（x）函數是對變量x進行循環遞增（當x超過最大值時，回歸到最小值）；Searched（S）函數返回1時，表示以S為根節點的子樹已經被搜索，否則返回0；Dead（S）返回1時表示以S為根節點的子樹中所有葉子節點都已經被遍歷，否則返回0.

2 驗證實例

為具體展示上述激勵方案的效果，本文選擇了IMEDiamond系統作為功能驗證實例.

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

由圖 5可以有以下結論：

1）相對所有的代碼覆蓋率，HSPC都能夠在很小的覆蓋率下發現同樣數目的功能bug；

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

3）最終覆蓋率收斂時，HSPC指導下發現的功能bug數要多于代碼覆蓋率.綜上可見，HSPC揭示功能bug的能力比傳統的代碼覆蓋率要更強大.

為比較不同的激勵生成算法所產生激勵與功能覆蓋率之間的關系，實驗比較了不同核數NC下為達到相同100% 的HSPC覆蓋率，本文結構化方法所需激勵數StructStiNum相對傳統隨機方法所需激勵數RanStiNum減少的比例ReduceRatio=1-StructStiNumRanStiNum，如圖6所示.

由圖 6可見，隨著核數的增加，ReduceRatio一直呈上升趨勢，即隨機化方法產生的激勵中冗余激勵的比例越來越高.NC=8時，ReduceRatio已經達到了96.3%.

此外在16核Intel Xeon E5520、主頻2.27 GHz、內存25 GB、Linux系統環境下，LeafNum及激勵生成時間（StrucTsti為結構化激勵時間，RanTsti為隨機激勵時間）與NC之間的關系統計如表1所示.

由表1可有以下結論：

1）激勵生成時間與LeafNum一樣，與NC之間都是指數增長關系，符合公式（2）.

2）在NC≤8時結構化激勵生成時間最大也就44 s，而隨機激勵已經到了3 883 s，是結構化方法的87倍.

3）本文的方法適合核數NC不是很大的多核系統，當NC超過8時，為了控制激勵生成時間，需要采取進一步的輸入空間化簡方法.

3 結 語

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

此外對于單核發起多個寫操作的情形，由于物理上不同的寫也是順序發起的，根據前述基本假設A6，每個寫都有各自對應的讀操作，所以可以根據不同寫發起的時間先后，將不同的寫劃歸入不同的時間片，每個時間片內每個核只有一個寫操作，此時本文的方法仍然適用.

參考文獻

[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] 胡偉武，夏培肅. 順序一致共享存儲系統中的亂序執行技術基本理論[J]. 計算機學報， 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] 王朋宇， 陳云霽，沈海華， 等. 片上多核處理器存儲一致性驗證[J]. 軟件學報， 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] 王志君，梁利平，吳凱 ，等.一種面向多媒體和通信應用的處理器指令集及架構實現[J].湖南大學學報（自然科學版）， 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一體化的處理器架構及其4核實現[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）