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

（華中科技大學(xué)電子科學(xué)與技術(shù)系，湖北 武漢430074）

1 引言

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

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

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

2 處理器驗(yàn)證方法

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

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

2.1 邊界值驗(yàn)證法

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

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

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

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

（4）健壯最壞情況驗(yàn)證法。當(dāng)對(duì)驗(yàn)證有特別極端的要求時(shí)，可以采用健壯最壞情況驗(yàn)證法。構(gòu)造了七個(gè)基礎(chǔ)值的笛卡爾積，如圖1d所示。對(duì)于n個(gè)輸入的驗(yàn)證對(duì)象，驗(yàn)證工作集的大小是7n。

Figure 1 Boundary value verification cases of bivariate object圖1 雙變量驗(yàn)證對(duì)象的邊界值驗(yàn)證案例示意圖

2.2 等價(jià)類驗(yàn)證法

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

從是否遵從單故障假設(shè)和是否關(guān)注無效數(shù)據(jù)和異常機(jī)制兩方面，分為四種等價(jià)類驗(yàn)證案例構(gòu)造方法，如圖2所示，分別對(duì)應(yīng)：

（1）弱一般等價(jià)類驗(yàn)證：基于單故障假設(shè)且不考慮無效值；

（2）強(qiáng)一般等價(jià)類驗(yàn)證：基于多故障假設(shè)且不考慮無效值；

（3）弱健壯等價(jià)類驗(yàn)證：基于單故障假設(shè)且考慮加入無效值；

（4）強(qiáng)健壯等價(jià)類驗(yàn)證：基于多故障假設(shè)且考慮加入無效值。

Figure 2 Equivalence class verification cases bivariate object圖2 雙變量驗(yàn)證對(duì)象的等價(jià)類驗(yàn)證案例示意圖

2.3 基于決策表驗(yàn)證法

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

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

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

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

2.4 綜合驗(yàn)證方法的選擇

針對(duì)微處理器不同功能部件的特點(diǎn)，微處理器綜合驗(yàn)證方法可結(jié)合上述三種驗(yàn)證方法，采用基準(zhǔn)驗(yàn)證法結(jié)合輔助驗(yàn)證法，生成高效的驗(yàn)證案例。

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

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

Table 2 Selection of function verification method表2 功能驗(yàn)證方法的選擇

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

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

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

4 高效能ESCA協(xié)處理器驗(yàn)證案例構(gòu)造

以具體的待測單元IALU、FMAC、DMA Engine為例，針對(duì)不同單元的特性，選擇合適的方法指導(dǎo)驗(yàn)證案例的手工生成和隨機(jī)驗(yàn)證案例生成的約束條件。

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

Figure 3 Diagram of ESCA system structure圖3 ESCA系統(tǒng)結(jié)構(gòu)框圖

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

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

4.1 邊界值驗(yàn)證法構(gòu)造IALU驗(yàn)證案例

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

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

IALU的輔助驗(yàn)證健壯性驗(yàn)證法用來補(bǔ)充異常和中斷驗(yàn)證，加入min－、max＋兩個(gè)取值點(diǎn)，此時(shí)對(duì)于操作數(shù)而言，沒有可以取值的對(duì)應(yīng)點(diǎn)，對(duì)于操作數(shù)來源，加入驗(yàn)證點(diǎn)R－1、R256。

4.2 等價(jià)類驗(yàn)證法構(gòu)造FMAC驗(yàn)證案例

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

對(duì)于基本浮點(diǎn)運(yùn)算指令，從輸入數(shù)據(jù)的角度，輸入驗(yàn)證狀態(tài)Din［8］為：

在輸出域的角度，將上述五種異常和正常情況對(duì)應(yīng)的關(guān)鍵數(shù)據(jù)集合分別記為：IOKEY、DZKEY、OFKEY、UFKEY、INEKEY、NORKEY，則輸出域驗(yàn)證集合RoutKEY為：

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

對(duì)于以上的等價(jià)類劃分，基準(zhǔn)驗(yàn)證法采用弱健壯等價(jià)類驗(yàn)證法，在每個(gè)等價(jià)類中選取相應(yīng)的驗(yàn)證點(diǎn)，并結(jié)合輔助驗(yàn)證法邊界值分析法，對(duì)于每個(gè)等價(jià)類如｛Dpn｝等，分別選取此類的邊界點(diǎn)加入驗(yàn)證案例。

4.3 決策表驗(yàn)證法構(gòu)造DMA功能單元驗(yàn)證案例

首先將DMA Engine輸入?yún)?shù)劃分等價(jià)類，根據(jù)廣播與否、讀寫情況、操作數(shù)由立即數(shù)或寄存器提供以及數(shù)據(jù)在buffer0或buffer1中操作幾個(gè)條件將驗(yàn)證空間劃分為16塊。如圖4所示，實(shí)心圓點(diǎn)對(duì)應(yīng)強(qiáng)一般等價(jià)類驗(yàn)證案例，空心圓點(diǎn)對(duì)應(yīng)弱一般等價(jià)類驗(yàn)證案例。

Figure 4 Division of equivaence class for DMA verification圖4 DMA驗(yàn)證的等價(jià)類劃分

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

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

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

5 高效能ESCA協(xié)處理器驗(yàn)證結(jié)果評(píng)測

針對(duì)高效能ESCA協(xié)處理器的不同功能單元，據(jù)其具體特性，可采用綜合驗(yàn)證法生成驗(yàn)證案例，如表4所示?；鶞?zhǔn)驗(yàn)證法與輔助驗(yàn)證法結(jié)合的綜合驗(yàn)證法，在達(dá)到功能驗(yàn)證目的的同時(shí)，能縮短驗(yàn)證時(shí)間并減少驗(yàn)證工作量。

Table 4 Comprehensive verification method of function units表4 功能單元綜合驗(yàn)證法

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

6 結(jié)束語

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

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

［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.

附中文參考文獻(xiàn)：

［3］ 王海霞.運(yùn)算電路的形式化驗(yàn)證方法研究［D］.北京：中國科學(xué)院計(jì)算技術(shù)研究所，2004.

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