高效能ESCA協(xié)處理器驗證技術研究＊

鄧承諾，吳 丹，黃 威，戴 葵，鄒雪城

（華中科技大學電子科學與技術系，湖北 武漢430074）

1 引言

隨著VLSI技術的進步，單芯片所能提供的豐富晶體管資源使得微處理器規(guī)模越來越大。而隨著微處理器規(guī)模的增大，體系結構日益復雜，多采用亂序執(zhí)行、多級流水、中斷、例外處理以及多級存儲結構等技術，使得處理器的驗證復雜度不斷增加。

在現(xiàn)代集成電路設計中，功能驗證所花的時間大概要占60%，功能驗證已經成為大規(guī)模集成電路設計的瓶頸［1］。用最少的驗證案例達到最大的驗證覆蓋率，盡可能地降低驗證成本和處理器面世時間是處理器驗證領域研究的核心問題。國內外對于加速處理器驗證和提高處理器驗證的完備性，做了很多相關研究，如驗證向量的自動生成［2］、形式化驗證技術［3］和覆蓋率分析［4］等。形式化驗證方法通過數學證明驗證系統(tǒng)的正確性，一般只用于規(guī)模不大的模塊級設計驗證；模擬方法用模擬矢量對 HDL（Hardware Description Language）描述的RTL（Register Transfer Level）模型進行模擬運行。目前，由于模擬驗證方法比較成熟，能適應規(guī)模越來越大的微處理器架構，因此仍然是微處理器驗證的主要手段。但是，不論是定向驗證激勵的產生還是隨機驗證激勵的自動生成，都只有在驗證方法學的指導下針對每個功能單元的特性，才能生成高效率的驗證案例，這正是本文要研究的內容。

本文借鑒軟件驗證的思想，將軟件功能驗證［5］中的邊界值驗證、等價類驗證和基于決策表的驗證應用于處理器驗證中，提出了一種針對微處理器不同功能部件特點設計微處理器綜合驗證方案的方法。該方法在完全實現(xiàn)微處理器驗證目標的同時，有效地縮短了驗證時間，提高了驗證效率，并已經成功應用于一款高效能協(xié)處理器ESCA的驗證中。

2 處理器驗證方法

微處理器驗證的目的是用最少的驗證案例覆蓋最大的待測功能，保證所有體系結構功能的正確性。本文主要采用基于模擬的驗證方法，通過模擬驗證案例集來驗證體系結構功能。驗證案例集一般包括隨機生成和手工生成的驗證案例，以及實際的應用程序工作負載。通過功能驗證方法指導驗證案例的手工生成和隨機驗證案例生成的約束條件，可提高驗證的覆蓋率和有效性。

功能驗證方法主要包括邊界值驗證、等價類驗證和基于決策表的驗證。

2.1 邊界值驗證法

邊界值驗證法通過考察輸入變量范圍的邊界值來構造驗證案例，衍生出四種技術：邊界值分析法、健壯性驗證法、最壞情況驗證法和健壯最壞情況驗證法。

（1）邊界值分析法。邊界值分析法利用輸入變量的最小值、略大于最小值的值、正常值、略小于最大值的值和最大值處的取值來構造驗證案例，并分別記為 min、min＋、nom、max－、max。圖1a所示是當兩個輸入變量x1∈［a，b］，x2∈［c，d］時的驗證案例選擇。當n個變量參與邊界值分析時，會產生4n＋1個不同的驗證案例。

（2）最壞情況驗證法。最壞情況驗證推翻單故障假設，考察多個變量同時取極值的情況，對min、min＋、nom、max－、max五個基本值取笛卡爾積構造驗證案例，如圖1b所示。對n個變量的驗證對象，會產生5n個驗證案例。最適合采用最壞情況驗證的場合是各個物理變量之間存在大量的相互作用，而且函數失效的代價極高。

（3）健壯性驗證法。健壯性驗證在邊界值分析法的基礎上，考察了略大于最大值（max＋）的值和略小于最小值（min－）的值，如圖1c所示。對于n個輸入的驗證對象，驗證狀態(tài)集合數為6n＋1。由于健壯性驗證把驗證的注意力部分集中在系統(tǒng)對異常情況的處理上，如例外和中斷處理，適用于存在大量異常處理的情況。

（4）健壯最壞情況驗證法。當對驗證有特別極端的要求時，可以采用健壯最壞情況驗證法。構造了七個基礎值的笛卡爾積，如圖1d所示。對于n個輸入的驗證對象，驗證工作集的大小是7n。

Figure 1 Boundary value verification cases of bivariate object圖1 雙變量驗證對象的邊界值驗證案例示意圖

2.2 等價類驗證法

等價類驗證法即根據輸入數據（或輸出狀態(tài)）的特性將其劃分為不同的等價類，在保證微處理器對于同一等價類的數據的處理相同的前提下，在一個等價類中選擇一個或多個關鍵數據構成驗證案例集。采用等價類驗證方法可很好地避免冗余，使驗證條理清晰，找到遺漏。

從是否遵從單故障假設和是否關注無效數據和異常機制兩方面，分為四種等價類驗證案例構造方法，如圖2所示，分別對應：

（1）弱一般等價類驗證：基于單故障假設且不考慮無效值；

（2）強一般等價類驗證：基于多故障假設且不考慮無效值；

（3）弱健壯等價類驗證：基于單故障假設且考慮加入無效值；

（4）強健壯等價類驗證：基于多故障假設且考慮加入無效值。

Figure 2 Equivalence class verification cases bivariate object圖2 雙變量驗證對象的等價類驗證案例示意圖

2.3 基于決策表驗證法

基于決策表驗證法是所有功能驗證法中最嚴格的，通過強化邏輯嚴密性，保證驗證的完整性和有效性。

該驗證法是通過分析被測程序各個功能之間的邏輯依賴關系編寫決策表，基于決策表生成驗證案例。如表1所示，決策表的樁條件項C1、C2、C3為輸入的等價類；樁動作項A1、A2、A3為處理器的功能；規(guī)則項為驗證案例；T／F表示是否滿足樁條件；“—”表示無關項，解釋為條件無關或不適用。

Table 1 Rule of decision table verification表1 決策表示意圖

對于n個樁條件，對應有2n個規(guī)則，而每出現(xiàn)m個無關項“—”規(guī)則項可擴展成2m個規(guī)則項。如表1所示，對應C1、C2、C3三個樁條件，應有八個規(guī)則項，而規(guī)則3、規(guī)則6分別相當于兩個規(guī)則項，故合并后的決策表共有六個規(guī)則項?！癤”代表適用對應的動作。

2.4 綜合驗證方法的選擇

針對微處理器不同功能部件的特點，微處理器綜合驗證方法可結合上述三種驗證方法，采用基準驗證法結合輔助驗證法，生成高效的驗證案例。

首先，根據待測功能單元輸入變量間是否存在依賴關系、是否遵從單故障假設以及是否存在大量的異常處理，根據表2選擇基準驗證方法。在表2中，C1、C2、C3是三個判斷的樁條件，A1～A9是九個對應處理的樁動作項，由三個樁條件可得出8個規(guī)則項，又由于規(guī)則5中無關項的存在，共有五個規(guī)則項。

其次，在基準驗證方法的基礎上，根據驗證對象靈活選取輔助驗證方法。以規(guī)則5為例，在C1條件不滿足、輸入不是獨立變量的情況下，只有A9決策表驗證法能被選作基準驗證方法，而此時結合A1邊界值分析法能驗證決策表中的規(guī)則邊界情況，因此選為輔助驗證方法，能提高驗證的覆蓋率。

Table 2 Selection of function verification method表2 功能驗證方法的選擇

3 高效能ESCA協(xié)處理器體系結構

ESCA（Engineering and Scientific Computing Accelerator）［6］是一款64位的高效能加速協(xié)處理器，它與通用處理器一起組成計算系統(tǒng)，基于主－協(xié)處理器協(xié)同工作的混合計算方式實現(xiàn)程序加速。其中協(xié)處理器ESCA采用單指令流多數據流SIMD（Single Instruction Multiple Data）的執(zhí)行方式，并行執(zhí)行工程與科學計算應用中可并行的核心程序，主機（HOST）執(zhí)行串行的計算指令和調度、分配任務。

ESCA主要針對的典型工作負載（Work Load）為科學計算、多媒體和數據庫等，其指令集結構分為三大類。其中，控制類指令主要包括條件、條件中斷、分支和系統(tǒng)控制及同步；數據傳輸類指令主要包括ESCA芯片和外部的Load／Store指令、計算陣列中PE以及組之間的數據傳輸指令；計算類指令主要包括定點ALU指令、定點邏輯指令和浮點指令。ESCA指令集采用128位定長固定格式指令編碼，指令中包含指令編碼、PE選擇掩碼、寄存器塊選擇掩碼及源、目的操作數。

4 高效能ESCA協(xié)處理器驗證案例構造

以具體的待測單元IALU、FMAC、DMA Engine為例，針對不同單元的特性，選擇合適的方法指導驗證案例的手工生成和隨機驗證案例生成的約束條件。

定點算術邏輯單元IALU指令，有兩到三個操作數輸入，操作數間無依賴關系，兩輸入值之間、輸入寄存器之間、以及輸入值和寄存器之間無大量的相互作用，遵從單故障假設，有上溢、下溢等簡單的異常處理，屬于表2中的規(guī)則項2。故基準驗證法可采用邊界值分析法，輔助驗證法采用健壯性驗證法進行異常與中斷驗證的補充。

Figure 3 Diagram of ESCA system structure圖3 ESCA系統(tǒng)結構框圖

多精度浮點功能單元FPU指令，與基本定點運算單元指令類似，操作數間無依賴關系且遵從單故障假設，但邊界情況多樣化，有非數、非規(guī)格數、正負無窮大等多種邊界，以及大量異常，屬于表2中的規(guī)則項1，適合進行等價類劃分。故基準驗證法采用弱健壯等價類驗證法，輔助驗證法采用邊界值分析法對等價類的劃分邊界進行補充驗證。

直接存儲訪問單元DMA Engine功能單元有18個輸入參數，輸入間有邏輯依賴關系，如根據廣播開啟位決定具體計算PE參數的采用與選擇；根據讀寫控制位決定讀寫掩碼的選擇來源，屬于表2中的規(guī)則項5?；鶞黍炞C法采用決策表驗證法，輔助驗證法采用強一般等價類驗證法將輸入狀態(tài)歸類以幫助生成決策表，并采用邊界值分析法補充驗證決策表每個規(guī)則項的邊界情況。

4.1 邊界值驗證法構造IALU驗證案例

IALU的基準驗證法（邊界值分析法）的取值點為 min、min＋、nom、max－、max，IALU的輸入包括操作數和操作數來源。以定點byte加為例，操作數分別用0x80、0x81、0x15、0x7e、0x7f來代入，對于操作數來源（寄存器名稱），則用R0、R1、R100、R254、R255代替。

從其鹿編來到編輯部的那天起，就注定要走上一條麻辣的不歸之路。以前能接受的帶有“麻辣”二字的食物只有麻辣拌、麻辣香鍋和麻辣小龍蝦，然后在外賣單上備注：不辣。剛來編輯部的時候，吃辣還吃得挺開心，直到有一天其鹿編吃了一塊不知什么品種的辣椒，開始不停地打嗝。以后只要看到小小的、油亮的紅色的東西，就不敢下筷子。后來還發(fā)現(xiàn)，經常吃辣還會讓臉長一種痘，而且很難消下去。所以其鹿編現(xiàn)在幾乎告別食辣了，但如果有哪位意絲未來想要成為編輯部的一員，可要學會吃辣呀，因為吃辣可以刺激食欲，編輯部的工作多得很，要多多吃飯以保存體力。

IALU的輔助驗證健壯性驗證法用來補充異常和中斷驗證，加入min－、max＋兩個取值點，此時對于操作數而言，沒有可以取值的對應點，對于操作數來源，加入驗證點R－1、R256。

4.2 等價類驗證法構造FMAC驗證案例

根據IEEE754［7］的標準，輸入數據分為非數集合DNaN、｛－∞｝、負的規(guī)格化非零浮點數集合Dnn、負的非規(guī)格化浮點數集合Dnd、｛－0｝、｛＋0｝、正的非規(guī)格化浮點數集合Dpd、正的規(guī)格化非零浮點數集合Dpn、｛＋∞｝。從輸出結果的角度，IEEE754標準定義了五種異常：無效操作、被零除、上溢、下溢、結果不精確。

對于基本浮點運算指令，從輸入數據的角度，輸入驗證狀態(tài)Din［8］為：

在輸出域的角度，將上述五種異常和正常情況對應的關鍵數據集合分別記為：IOKEY、DZKEY、OFKEY、UFKEY、INEKEY、NORKEY，則輸出域驗證集合RoutKEY為：

輸入輸出域的驗證狀態(tài)集合DinKEY×RoutKEY即為滿足要求的驗證案例集。

對于以上的等價類劃分，基準驗證法采用弱健壯等價類驗證法，在每個等價類中選取相應的驗證點，并結合輔助驗證法邊界值分析法，對于每個等價類如｛Dpn｝等，分別選取此類的邊界點加入驗證案例。

4.3 決策表驗證法構造DMA功能單元驗證案例

首先將DMA Engine輸入參數劃分等價類，根據廣播與否、讀寫情況、操作數由立即數或寄存器提供以及數據在buffer0或buffer1中操作幾個條件將驗證空間劃分為16塊。如圖4所示，實心圓點對應強一般等價類驗證案例，空心圓點對應弱一般等價類驗證案例。

Figure 4 Division of equivaence class for DMA verification圖4 DMA驗證的等價類劃分

在等價類劃分的基礎上，同樣根據廣播與否、讀寫情況、操作數由立即數或寄存器提供以及數據在buffer0或buffer1中操作幾個條件編寫決策表，如表3所示。

考慮到無關項，共有12個規(guī)則項。根據決策表，對應每個規(guī)則項生成相應的驗證案例。再采用邊界值分析法對于每個規(guī)則項對應的起始地址、傳輸長度、傳輸跳步與讀寫掩碼生成輔助的驗證案例。

Table 3 Decision table verification cases of DMA fuction units表3 DMA Engine功能單元決策表驗證案例

5 高效能ESCA協(xié)處理器驗證結果評測

針對高效能ESCA協(xié)處理器的不同功能單元，據其具體特性，可采用綜合驗證法生成驗證案例，如表4所示?；鶞黍炞C法與輔助驗證法結合的綜合驗證法，在達到功能驗證目的的同時，能縮短驗證時間并減少驗證工作量。

Table 4 Comprehensive verification method of function units表4 功能單元綜合驗證法

全完備驗證是遍歷所有的驗證狀態(tài)、每一個操作數可能的取值得到的驗證案例集。如圖5所示，綜合驗證法與全完備驗證相比，驗證數量和效率得到了大幅提升。在設計仿真后期，由于驗證激勵要反復使用，以驗證不斷修改完善的處理器功能的正確性，因此高效的驗證案例集節(jié)約了大量的驗證時間，并能同時保證驗證的完備性和覆蓋率［9］。

6 結束語

Figure 5 Verification cases scale comparison of function units圖5 部分功能單元驗證案例規(guī)模比較

處理器的功能驗證是非常復雜的系統(tǒng)工程，在ESCA處理器的驗證中，主要采用了基于模擬的驗證方法，通過設計方案與C語言實現(xiàn)的黃金參考模型構建的自動驗證平臺完成驗證流程。本文主要在邊界值驗證法、等價類驗證法、決策表驗證法的基礎上，提出了一種針對微處理器不同功能部件特點設計微處理器綜合驗證案例的方法，探討不同功能單元的綜合驗證方法對應的基準驗證方法與輔助驗證方法，并在與全完備驗證的比較中驗證其高效性。本文給出的綜合驗證法通過實際驗證保證功能100%驗證，覆蓋指令集所有指令和每條指令的異常、正常執(zhí)行情況，發(fā)現(xiàn)了浮點功能單元的精度誤差、異常處理錯誤等問題，以及DMA和網絡部分的跳步、掩碼錯誤等問題，進行了及時的更正，保證了流片的成功。

［1］ Evans A，Silburt A.Functional verification of large ASICs［C］∥Proc of the 35th Design Automation Conference，1988：650－655.

［2］ Aharon A，Goodman D.Test program generation for functional verification of power PC processors in IBM［C］∥Proc of the 32nd Design Automation Conference，1995：279－285.

［3］ Wang Hai－xia.Research on formal methods in arithmetic circuit verification［D］.Beijing：Institute of Computing Technology，2004.（in Chinese）

［4］ Benjamin M.A study in coverage－driven test generation［C］∥Proc of the 36th Design Automation Conference，1999：970－975.

［5］ Jorgensen P C.Software testing：A craftman’s approach［M］.Boca Raton：CRC Press，1995.

［6］ Pan Chen，Kui Dai，Dan Wu，et al.Parallel algorithms for FIR computation mapped to ESCA architecture［C］∥Proc of 2010International Conference of Information Engineering，2010：123－126.

［7］ IEEE Standard for Binary Float－Point Arithmetic［S］.NY：The Institute of Electrical and Electronics Engineers，1985.

［8］ Qu Ying－jie，Xia Hong，Wang Qin.A research of functional testing method for microprocessor floating－point arithmetic J .Computer Engineering and Applications2001742－43.（in Chinese）

［9］ Ur S，Yadin Y.Micro architecture coverage directed generation of test programs［C］∥Proc of the 36th Design Automation Conference，1999：175－180.

附中文參考文獻：

［3］ 王海霞.運算電路的形式化驗證方法研究［D］.北京：中國科學院計算技術研究所，2004.

［8］ 曲英杰，夏宏，王沁.微處理器浮點去處功能的測試方法研究［J］.計算機工程與應用，2001（7）：42－43.