楊修濤，谷小秋

（北京電子工程總體研究所，北京100854）

基于指令的數(shù)字信號(hào)處理器驗(yàn)證

楊修濤，谷小秋

（北京電子工程總體研究所，北京100854）

針對(duì)數(shù)字信號(hào)處理器設(shè)計(jì)中因相關(guān)引發(fā)的故障，提出一種基于指令的驗(yàn)證方法。結(jié)合處理器的體系結(jié)構(gòu)特點(diǎn)給出處理器表示矩陣，并利用該矩陣，根據(jù)所使用的功能單元對(duì)指令進(jìn)行劃分。在同一個(gè)劃分內(nèi)，指令使用相同的功能單元，對(duì)這些指令進(jìn)行兩兩組合，生成驗(yàn)證指令序列。考慮測(cè)試的可觀測(cè)性給出觀測(cè)方法，從理論上證明該方法可以完備覆蓋到所有數(shù)據(jù)相關(guān)故障。設(shè)計(jì)驗(yàn)證指令生成系統(tǒng)自動(dòng)生成驗(yàn)證指令序列，針對(duì)DSPC-01處理器進(jìn)行實(shí)驗(yàn)，并與流片后的測(cè)試結(jié)果比較分析，結(jié)果驗(yàn)證了該方法的有效性。

驗(yàn)證；數(shù)字信號(hào)處理器；數(shù)據(jù)相關(guān)；指令生成；覆蓋率；自動(dòng)生成

1 概述

數(shù)字信號(hào)處理器（Digital Signal Processor，DSP）已被應(yīng)用于多種領(lǐng)域，針對(duì)數(shù)字信號(hào)處理器的研發(fā)日益增多。同時(shí)，電路的規(guī)模也越來(lái)越大，相應(yīng)的針對(duì)這些復(fù)雜設(shè)計(jì)的驗(yàn)證也越來(lái)越困難。有關(guān)DSP驗(yàn)證與測(cè)試的研究主要集中于DSP的二次開發(fā)驗(yàn)證上，比如以DSP作嵌入式開發(fā)的設(shè)計(jì)等。這樣，相當(dāng)?shù)尿?yàn)證工作主要集中于外圍外電路上面，以及外圍電路與DSP之間的總線、協(xié)議上。比如一款基于DSP芯片開發(fā)的手機(jī)，驗(yàn)證的重點(diǎn)為總線仲裁、射頻模塊、數(shù)模轉(zhuǎn)換以及一些其自帶嵌入式操作系統(tǒng)及軟件。換而言之，這類工作都沒(méi)去考慮或涉及DSP核本身的驗(yàn)證、測(cè)試。對(duì)DSP核的驗(yàn)證則是由幾大DSP生產(chǎn)廠商（TI，ADI，M otorola）和學(xué)術(shù)機(jī)構(gòu)進(jìn)行研究的。這類工作由于技術(shù)保密等原因，相關(guān)論文相對(duì)比較少，而且論述也比較簡(jiǎn)略或籠統(tǒng)。文獻(xiàn)［1］以TMS320C5為例給出了在寄存器傳輸級(jí)（Register Transfer Level，RTL）對(duì)DSP進(jìn)行驗(yàn)證的方法。文獻(xiàn)［2-3］使用了形式驗(yàn)證方法。首先，將DSP按模塊的不同進(jìn)行劃分，針對(duì)每個(gè)功能模塊給出相應(yīng)的邏輯形式；然后，將上述邏輯用高階邏輯（High Order Logic，HOL）的形式進(jìn)行描述［4］；最后，使用相應(yīng)HOL工具對(duì)編碼進(jìn)行編譯運(yùn)行，由機(jī)器自動(dòng)推理邏輯上的正確與否［5］。這種方法的優(yōu)點(diǎn)是邏輯性強(qiáng)、可靠性高、經(jīng)過(guò)驗(yàn)證的電路模塊邏輯上是肯定的。但在實(shí)際應(yīng)用中，將整個(gè)DSP設(shè)計(jì)全部以邏輯形式描述出來(lái)，需要耗費(fèi)大量的人力，同時(shí)機(jī)器證明的速度比較慢，中間可能需要人工干預(yù)。對(duì)于一款有流水結(jié)構(gòu)的DSP來(lái)說(shuō)，被用于驗(yàn)證通用處理器設(shè)計(jì)的方法［6］，略作修改后也可以適用于該DSP的驗(yàn)證。目前，這方面的研究相比起DSP的驗(yàn)證來(lái)要多很多。它們或者是從指令功能方面對(duì)處理器加以驗(yàn)證，或從流水方面對(duì)處理器加以驗(yàn)證。文獻(xiàn)［7］從另一個(gè)角度考慮處理器設(shè)計(jì)中所產(chǎn)生的bug以及驗(yàn)證問(wèn)題。考慮到指令集太大，文獻(xiàn)［8］給出了化簡(jiǎn)方法?；旧?，針對(duì)有流水結(jié)構(gòu)設(shè)計(jì)的處理器的驗(yàn)證不可避免的涉及到一個(gè)概念：相關(guān)。后面會(huì)給出其定義。

根據(jù)引起相關(guān)的原因，可以把指令間的相關(guān)分為3種：數(shù)據(jù)相關(guān)，控制相關(guān)，結(jié)構(gòu)相關(guān)。對(duì)于數(shù)據(jù)相關(guān)問(wèn)題，在硬件設(shè)計(jì)中常常是采用一些專門的方法來(lái)解決。比如，在解決寫后讀（Read A fter W rite，RAW）時(shí)，可以采用Forw arding技術(shù)。除此之外，對(duì)于數(shù)據(jù)相關(guān)的指令還可以采用靜態(tài)調(diào)度的方法來(lái)解決。但在驗(yàn)證所設(shè)計(jì)的處理器時(shí)，卻恰恰相反，需要有針對(duì)性的數(shù)據(jù)相關(guān)生成指令來(lái)對(duì)處理器進(jìn)行功能驗(yàn)證。有關(guān)這方面的論述，較早的有文獻(xiàn)［9］，文中主要針對(duì)處理器的功能驗(yàn)證、測(cè)試進(jìn)行論述，提出了指令分解、運(yùn)算及錯(cuò)誤判定方法。同時(shí)提及相關(guān)指令的測(cè)試、驗(yàn)證問(wèn)題。特別針對(duì)相關(guān)問(wèn)題進(jìn)行描述的有文獻(xiàn)［10］，該文首先給出了根據(jù)功能單元進(jìn)行列表的思想，依據(jù)所列出的指令、功能單元相關(guān)矩陣來(lái)判斷指令間的相關(guān)性。文獻(xiàn)［11］對(duì)流水中數(shù)據(jù)相關(guān)進(jìn)行了更進(jìn)一步的描述，它將相關(guān)矩陣的思想引入，再根據(jù)流水的特點(diǎn)，對(duì)指令的進(jìn)一步劃分進(jìn)行了更細(xì)致的闡述，最后生成能驗(yàn)證相關(guān)故障的指令集。文獻(xiàn)［10-11］方法主要是基于相關(guān)矩陣，該矩陣被命名為處理器表示矩陣（Processor Representation M atrix，PRM）。本文在上述研究工作的基礎(chǔ)上，結(jié)合一款自主設(shè)計(jì)的DSP處理器核（DSPC-01）架構(gòu)特點(diǎn)，給出驗(yàn)證指令生成方法。

2 相關(guān)工作

定義1 在流水線中，如果某條指令的某個(gè)階段必須等到它前面另一條指令的某個(gè)階段后才能開始，則這兩條指令間存在相關(guān)［12］。

定義2 處理器表示矩陣（PRM）

一個(gè)PRM是N×M矩陣，其中，N表示該處理器的指令數(shù)；M表示該處理器的功能單元數(shù)［11］。該矩陣包含的元素及含義如表1所示。

表1 PRM元素含義

根據(jù)表1定義，給出DSPC-01的PRM。DSPC-01是一款自主設(shè)計(jì)的DSP，支持基本的DSP指令。它的功能單元主要包括：2個(gè)寄存器堆X和Y，共有16個(gè)寄存器（XR0～XR15，YR0～YR15）、2個(gè)算術(shù)運(yùn)算器、2個(gè)整數(shù)算術(shù)運(yùn)算器、1個(gè)乘法器、1個(gè)移位器等。支持常用的ADD，SUB，MUL以及移位等指令。表2給出了DSPC-01中1條加法運(yùn)算指令及其在PRM矩陣中對(duì)應(yīng)行的簡(jiǎn)化表示形式。其中，行表示指令行；列表示功能單元列；XR為X計(jì)算塊中的寄存器，YR為Y計(jì)算塊中的寄存器；ALU1為X計(jì)算塊的ALU功能單元，ALU2為Y計(jì)算塊的ALU功能單元；T，R表示該寄存器既發(fā)出數(shù)據(jù)又接收數(shù)據(jù)；M1則表示為ADD操作，在PRM建立過(guò)程中可以根據(jù)需要定義。如可以將ADD操作定義為M1，SUB操作定義為M2。

表2 ADD指令的PRM表示

DSPC-01處理器與一般通用處理器有些不同，它有2個(gè)計(jì)算塊。因此，分別有2個(gè)ALU及相關(guān)寄存器堆，表現(xiàn)在表2上就是ALU 1對(duì)應(yīng)著寄存器堆XR及操作M1，ALU2對(duì)應(yīng)寄存器堆YR及操作M1。在后面中，所有類同的指令均會(huì)有相同的表現(xiàn)。在此基礎(chǔ)上，本文給出DSPC-01的PRM構(gòu)造方法。

2.1 DSPC-01處理器及指令集

DSPC-01是一個(gè)具有128位數(shù)據(jù)總線，支持超長(zhǎng)指令字（Very Long Instruction Word，VLIW）的超標(biāo)量數(shù)字信號(hào)處理器。分別對(duì)稱地?fù)碛?個(gè)ALU（ALU1，ALU2）、2個(gè)移位器（SHF1，SHF2）、3個(gè)2 MB的寄存器堆（一個(gè)為指令寄存器堆，另兩個(gè)分別為XR和YR）、2個(gè)乘法器（MUL1，MUL2）以及2個(gè)整數(shù)ALU（IALU1，IALU2）。

為直觀起見，將DSPC-01的指令按功能類型劃分為6類：ALU，CLU，MUL，SHIFT，IALU和BRANCH。

需要說(shuō)明的是，在DSPC-01的具體實(shí)現(xiàn)中CLU指令是在ALU中進(jìn)行執(zhí)行的，所以，這兩部分指令可以統(tǒng)一劃歸于ALU中。對(duì)于IALU，它同ALU一樣，也是有2個(gè)計(jì)算塊，所不同的是在IALU中，它分為XI和Y I計(jì)算塊，而對(duì)應(yīng)的其計(jì)算塊中的寄存器堆也變成X IR0～X IR15，YIR0～Y IR15。這樣，可以考慮將XI和YI兩塊分開來(lái)分析。部分DSPC-01指令列表如表3所示。

表3 DSPC-01指令列表（部分）

指令集中所涉及到的功能單元主要有：XR，YR，ALU1，ALU，ALU2，CLU，MUL1，MUL2，SHF1，SHF2，XIR，YIR，IALU1，IALU2，PC，LC0，LC1，XSTAT，YSTAT，CJ，ACC，SFR以及RAM。其中，XR，YR為ALU的寄存器。ALU1～ALU2為2個(gè)ALU單元，MUL1～MUL2為2個(gè)乘法單元。SHIFTER1～2為2個(gè)移位器單元，X IR/Y IR分別為IALU1/IALU2中寄存器堆。RAM為M emory，SFR為條件寄存器SFREG。

2.2 DSPC-01的PRM及指令劃分

根據(jù)表3和功能單元可以構(gòu)造出DSPC-01的PRM，該P(yáng)RM的行剛好由表3中的所有指令組成，而列則由所有功能單元組成。由此，可以得到一個(gè)N（指令數(shù)）×M（功能單元數(shù)）矩陣。在此基礎(chǔ)上，下面給出等價(jià)寄存器與等價(jià)寄存器集的概念。

定義3 等價(jià)寄存器

2個(gè)寄存器對(duì)于一個(gè)指令集I是等價(jià)的，當(dāng)且僅當(dāng)對(duì)于該指令集中任何一條指令，使用一個(gè)寄存器（在給定的取址模式下）作為操作數(shù)與將其替換為另一個(gè)寄存器作為操作數(shù)一樣［9］。

定義4 等價(jià)寄存器集

如果一個(gè)寄存器集合中任意2個(gè)寄存器都滿足上述定義，則稱該集為等價(jià)寄存器集［9］。

根據(jù)定義3和定義4不難判斷，XR0-XR30彼此之間是等價(jià)寄存器，因此XR則為等價(jià)寄存器集。同理，YR，X IR，Y IR均是等價(jià)寄存器集。對(duì)等價(jià)寄存器與等價(jià)寄存器集的定義，旨在于為以后驗(yàn)證指令生成提供證明，即：對(duì)于給定的一條指令，使用XR0與XR1是等價(jià)的，因此，推廣開來(lái)，可以使用XR0，XR1，XR2來(lái)表示對(duì)XR寄存器的使用。

定義5 假設(shè)i為指令集I中的一條指令，則Ri=｛r1，r2，…，rn｝稱為該指令所使用的寄存器集，其中，rK，K∈1，2，…，n為定義4中的等價(jià)寄存器集或該等價(jià)寄存器集中的一個(gè)寄存器。

如無(wú)特別說(shuō)明，當(dāng)某條指令用到某一等價(jià)寄存器時(shí)，使用等價(jià)寄器集來(lái)代替。

3 指令自動(dòng)生成算法

3.1 分類算法

根據(jù)定義4可以給出指令的劃分算法，劃分依據(jù)是指令所用寄存器集的異同。

同一劃分內(nèi)的任意2條指令，它們使用完全相同的寄存器集，如果2條指令在流水中相鄰出現(xiàn)，必定會(huì)引起數(shù)據(jù)相關(guān)。因此，可以依據(jù)這樣的劃分，在每一個(gè)劃分內(nèi)，對(duì)所有的指令作組合。如果，將存在數(shù)據(jù)相關(guān)關(guān)系的2條指令用一條邊連接，指令作為一個(gè)節(jié)點(diǎn)，那么，一個(gè)劃分內(nèi)的所有指令組成一個(gè)完全圖。依序遍歷所有的邊，可以得到數(shù)據(jù)相關(guān)的驗(yàn)證指令集，當(dāng)然該集是針對(duì)該劃分內(nèi)所有指令的共同寄存器的。對(duì)所有的劃分進(jìn)行上述工作可以得到整個(gè)指令集內(nèi)所有劃分的驗(yàn)證指令集。

除此之外，假設(shè)這2條指令為i1，i2，它們滿足如下關(guān)系：（1）Ri1≠Ri2；（2）Ri1∩Ri2≠φ。即：這2條指令不在同一劃分內(nèi)，但部分地使用相同的寄存器。顯然，由于存在使用相同寄存器的情況，因此，這2條指令之間是可能存在數(shù)據(jù)相關(guān)的。對(duì)這一部分指令的處理辦法是：將它們所在的2個(gè)集合，比如：對(duì)S1，S2做S1×S2運(yùn)算。假設(shè)：S1=（i1，i2，…，in），S2=（j1，j2，…，jm），則有它們的笛卡爾乘積S1× S2=（〈i1，j1〉，〈i1，j2〉，…，〈in，jm〉）。由于使用相同寄存器的指令都潛在的存在數(shù)據(jù)相關(guān)，因此作S1× S2運(yùn)算可以保證所有可能存在數(shù)據(jù)相關(guān)的故障在理論上均被覆蓋到。

3.2 指令生成

3.2.1 一拍相關(guān)的測(cè)試指令生成

上面給出了指令劃分的方法，并且給出了存在數(shù)據(jù)相關(guān)的指令間的關(guān)系。由此可知，若要生成存在數(shù)據(jù)相關(guān)關(guān)系的驗(yàn)證指令，需要處理2種集合關(guān)系：一種是劃分集合內(nèi)部的指令間關(guān)系，另一種是需要做乘積運(yùn)算的集合內(nèi)部指令間關(guān)系。以集合S1，S2為例。同一劃分集合內(nèi)的指令，它們之間需要做兩兩組合，事實(shí)上這種關(guān)系依然可以表示為該劃分集合乘積運(yùn)算：S1×S2。這樣就存在2種需要分析的情況：（1）S1×S1；（2）S1×S2。滿足第（1）種情況的指令，它們的關(guān)系在劃分集合內(nèi)部構(gòu)成一個(gè)完全圖。例如，假設(shè)在集合S1內(nèi)部有4條指令i1～i4，那么以指令為節(jié)點(diǎn)，可以構(gòu)成如圖1所示的完全圖。

圖1 由4條指令構(gòu)成的完全圖

任意2條指令i，j，i與j之間存在數(shù)據(jù)相關(guān)的關(guān)系，所以，應(yīng)該存在一條有向邊i→j，同樣，j與i之間也存在數(shù)據(jù)相關(guān)的關(guān)系，所以，亦存在有向邊j→i。就是說(shuō)，實(shí)際上是i，j之間存在2條有向邊。因此，在圖1中可以化簡(jiǎn)為無(wú)向邊。遍歷這些邊，顯然可以得到指令之間的數(shù)據(jù)相關(guān)關(guān)系。比如，遍歷i，j可以得到有向邊i→j；遍歷j，i可以得到j(luò)→i。圖1所示的完全圖實(shí)際上是遍歷每條邊2次。不妨假設(shè)這4個(gè)節(jié)點(diǎn)分別被標(biāo)記為i1，i2，i3，i4，那么會(huì)有下列遍歷情況：

理論上，所有的邊均應(yīng)該被遍歷2次，但是考慮到指令是在流水線中出現(xiàn)相關(guān)，即指令間是存在順序關(guān)系的。那么分析式（1）和式（2）可以看出，若由式（1）列出驗(yàn)證指令集（指令序列），那么可以得到：

指令在流水線中執(zhí)行的情形如圖2所示，其中，虛線表示需要補(bǔ)充的一種指令組合關(guān)系。

圖2 指令在流水線中被執(zhí)行示例

將式（3）與式（1）、式（2）對(duì)比可知，實(shí)際上在一次的遍歷中已覆蓋了大部分相關(guān)情況，只需要再補(bǔ)充一個(gè)相關(guān)關(guān)系i4→i1即可。因此，沒(méi)有必要遍歷2次。整個(gè)的測(cè)試生成的算法描述如下：

算法 指令生成

輸入 初步建立好的PRM，記為MA（這是完全根據(jù)DSPC-01的架構(gòu)初步手工編寫的處理器表示矩陣，沒(méi)有作其他處理，需要后續(xù)的算法處理）

輸出 Sc

3.2.2 多拍相關(guān)的驗(yàn)證指令生成

在上面中只給出了一拍數(shù)據(jù)相關(guān)的測(cè)試指令生成方法。對(duì)于DSPC-01，它的流水線深度為8，其中前3拍為取指IF1，IF2，IF3，后5拍分別為D，I，A，EX 1，EX 2。這樣，流水最多可能會(huì)存在4拍相關(guān)。根據(jù)DSPC-01的指令特點(diǎn)，能引起多拍數(shù)據(jù)相關(guān)的指令主要有如下情況：（1）總線沖突相關(guān)，一般有2拍相關(guān)；（2）計(jì)算塊載入的相關(guān)，最多可能4拍相關(guān)；（3）IALU加載相關(guān)，最多可能3拍相關(guān)；（4）外部存儲(chǔ)器載入相關(guān)，最多可引起4拍相關(guān)；（5）條件IALU加載相關(guān)，最多可能引起4拍相關(guān)。

針對(duì)上述5種類型的指針做多拍相關(guān)的驗(yàn)證指令生成，可以滿足檢測(cè)到指令集中可能存在的多拍相關(guān)。對(duì)于多拍相關(guān)，問(wèn)題所關(guān)注的只是隔開多少拍后兩條指令依然存在相關(guān)，因此，2條指令之間插入1個(gè)～4個(gè)NOP指令即可。

3.3 可觀測(cè)性分析

考慮可觀測(cè)性時(shí)，可測(cè)性設(shè)計(jì)（Design For Testability，DFT）還不可用，所以，使用DFT以外的方法來(lái)實(shí)現(xiàn)觀測(cè)驗(yàn)證結(jié)果的目的。在實(shí)際應(yīng)用中是借用了DSP的3個(gè)靜態(tài)存儲(chǔ)器（Static Random Access M emory，SRAM）中的一個(gè)來(lái)暫存指令運(yùn)行結(jié)果。

由于在驗(yàn)證過(guò)程中，指令需要存儲(chǔ)在指令RAM中，因此只能選擇2個(gè)數(shù)據(jù)RAM來(lái)存儲(chǔ)指令運(yùn)行結(jié)果，如圖3所示，其中一個(gè)存放的是指令運(yùn)行過(guò)程中需要用到的數(shù)據(jù)，比如數(shù)據(jù)存儲(chǔ)器RAM_A，所以選擇另外一個(gè)數(shù)據(jù)存儲(chǔ)器RAM_B來(lái)存儲(chǔ)運(yùn)行的結(jié)果。在指令運(yùn)行完后，將結(jié)果從RAM_B中導(dǎo)出進(jìn)行比對(duì)，以觀測(cè)指令執(zhí)行的結(jié)果。對(duì)于兩拍以上相關(guān)的指令，由于中間可以插NOP，因此使用的是插入額外的其他指令來(lái)觀測(cè)運(yùn)行結(jié)果。所以，對(duì)其觀測(cè)更容易。

圖3 DSP中的3塊RAM

4 實(shí)驗(yàn)及結(jié)果分析

由數(shù)據(jù)相關(guān)定義可知：指令間存在數(shù)據(jù)相關(guān)的原因是由于使用了同一寄存器。由此，可以直接推出以下推論：

推論 在流水線中，如果2條指令存在數(shù)據(jù)相關(guān)，那么它們一定使用了相同的寄存器。

進(jìn)一步分析：對(duì)于任一可能的單拍數(shù)據(jù)相關(guān)，上述方法是否都能生成一個(gè)指令組合以覆蓋到該數(shù)據(jù)相關(guān)。

命題 對(duì)于任一由2條相鄰指令所形成的數(shù)據(jù)相關(guān)，上述方法總能給出一個(gè)指令組合以覆蓋到該相關(guān)關(guān)系。

證明：假設(shè)，存在2條指令ij，iK，它們所在的劃分集合分別為Sij，SiK。同時(shí)，它們之間有數(shù)據(jù)相關(guān)關(guān)系，但卻不能被上述方法檢測(cè)到，那么它們一定滿足：（1）不在同一劃分集中；（2）各自所在的劃分集中的指令彼此都沒(méi)有使用任何相同的寄存器。否則：

如果它們不滿足條件（1），那么它們?cè)谕粍澐种?，即：Sij=SiK，這樣在同一劃分中一定會(huì)有組合ij→iK和iK→ij能覆蓋到該相關(guān)關(guān)系。因此，它一定滿足條件（1），所以有Rij≠RiK。

如果它們不滿足條件（2），那么由于同一劃分中的指令一定會(huì)使用完全相同的寄存器，所以，應(yīng)該有Rij≠RiK，Rij∩RiK≠φ。即：這兩條指令組合一定會(huì)出現(xiàn)在Sij×SiK中。

該2條指令一定能同時(shí)滿足條件（1）和條件（2），即Rij≠RiK，Rij∩RiK=φ，而這2條指令間又存在數(shù)據(jù)相關(guān)關(guān)系，這與推論相矛盾。

證畢。

上面只是從理論方面證明了該算法是有效的，下面給出相應(yīng)的實(shí)驗(yàn)及實(shí)驗(yàn)結(jié)果。為了生成驗(yàn)證指令的需要，項(xiàng)目過(guò)程中，采用C++編寫了一個(gè)針對(duì)DSP的驗(yàn)證指令生成系統(tǒng)（Verification Instruction Automatic Generation System，V IAGS）。最終生成的結(jié)果文件中C.asm包含指令9 067條，B.asm中包含指令8 993條，共計(jì)指令18 060條。分別以C.asm和B.asm指令集作為激勵(lì)，施加到DSPC-01進(jìn)行驗(yàn)證。為了加快驗(yàn)證進(jìn)程，將邏輯設(shè)計(jì)分塊后并行驗(yàn)證，結(jié)果如表4所示，該表為設(shè)計(jì)中實(shí)際存在的bug，非手工插入。

表4 各模塊驗(yàn)證結(jié)果

由3.3節(jié)的可觀測(cè)性分析中可知，表4中的數(shù)據(jù)是在指令序列全部運(yùn)行完后統(tǒng)計(jì)出的。同一個(gè)bug可能會(huì)被統(tǒng)計(jì)到多次，所以，需要在回歸驗(yàn)證過(guò)程中進(jìn)行篩選。最終回歸驗(yàn)證收斂后統(tǒng)計(jì)出的bug數(shù)（非重復(fù)）結(jié)果如表5所示。

表5 最終驗(yàn)證檢測(cè)到的實(shí)際bug個(gè)數(shù)

將表4、表5的結(jié)果進(jìn)行比較，如圖4所示?？梢钥闯?，表4、表5的bug數(shù)量趨勢(shì)一致，基本上最初報(bào)出bug較多的模塊，實(shí)際bug也較多。在實(shí)際驗(yàn)證過(guò)程中針對(duì)最初報(bào)出bug較多的模塊有必要加強(qiáng)驗(yàn)證。

圖4 bug個(gè)數(shù)對(duì)比

在芯片流片后，針對(duì)相應(yīng)的芯片進(jìn)行進(jìn)一步的測(cè)試分析，測(cè)試過(guò)程中，除了使用上述的指令集外，還引入一些實(shí)際的Benchmark以及大量的實(shí)際應(yīng)用來(lái)對(duì)DSPC-01進(jìn)行測(cè)試，檢驗(yàn)本文方法是否有效。表6給出了部分用例。

表6 成片測(cè)試結(jié)果

為了進(jìn)一步檢驗(yàn)效果，在DSPC-01的驗(yàn)證過(guò)程中，采用先用其他驗(yàn)證方法驗(yàn)證，然后用本文方法檢驗(yàn)的策略。如果本文方法生成的驗(yàn)證指令集能在已驗(yàn)證過(guò)的模塊上繼續(xù)發(fā)現(xiàn)bug，那么也能證明本文方法針對(duì)驗(yàn)證是有效的，結(jié)果如表7所示。

表7 本文方法結(jié)果

可以看到，用B.asm和C.asm共繼續(xù)檢測(cè)到4個(gè)未被發(fā)現(xiàn)的bug，經(jīng)過(guò)2個(gè)版本的實(shí)驗(yàn)結(jié)果比較，證明本方法針對(duì)驗(yàn)證是有效的。

總體上看，該方法是實(shí)現(xiàn)了對(duì)處理器的功能驗(yàn)證。對(duì)于有RTL代碼的自主設(shè)計(jì)以及第三方IP核均可達(dá)到驗(yàn)證功能的目的。

5 結(jié)束語(yǔ)

本文主要完成了以下工作：（1）針對(duì)DSPC-01的架構(gòu)建立處理器表示矩陣，并進(jìn)行分塊和劃分；（2）基于處理器矩陣的概念，給出相應(yīng)的算法，生成針對(duì)DSPC-01的驗(yàn)證指令集。（3）設(shè)計(jì)V IAGS驗(yàn)證指令生成系統(tǒng)，并對(duì)驗(yàn)證指令集的驗(yàn)證過(guò)程進(jìn)行了比較、分析。

在未來(lái)的工作中，將進(jìn)一步研究針對(duì)網(wǎng)表級(jí)的驗(yàn)證，研究在等價(jià)寄存器這一概念不再成立時(shí)的驗(yàn)證指令集生成方法，并加強(qiáng)可觀測(cè)性分析和設(shè)計(jì)，從而做到隨時(shí)觀測(cè)指令運(yùn)行結(jié)果，便于及時(shí)分析、查找設(shè)計(jì)錯(cuò)誤。同時(shí)對(duì)所有的指令模式進(jìn)行等價(jià)性分析及合并，以便能生成更為簡(jiǎn)短的驗(yàn)證指令集。

［1］ Gl?kler T，Bitterlich S，Meyr H.DSP Core Verification Using Automatic Test Case Generation［C］//Proceedings of IEEE International Conference on Acoustics，Speech，and Signal Processing.Washington D.C.，USA：IEEE Press，2000：3271-3274.

［2］ Habibi T，Tahar S，Ghazel A.Formal Modelling of the ADSP-2100 Processor Using HOL［C］//Proceedings of IEEE Canadian Conference on Electrical&Computer Engineering.Washington D.C.，USA：IEEE Press，2002：614-619.

［3］ Habibi T，Tahar S，Ghazel A.Formal Verication of a DSP Chip Using an Iterative Approach［C］//Proceedings of Euromicro Symposium on Digital System Design.Washington D.C.，USA：IEEE Press，2002：12-19.

［4］ Habibi T，Tahar S，Ghazel A.Formal Verication of the ADS-2100 Processor Using the HOL Theorem Prover［Z］. 2002.

［5］ Akbarpour B，Tahar S.An Approach for the Formal Verication of DSP Designs Using Theorem Proving［J］. IEEE Transactions on CAD of Integrated Circuits and System s，2006，25（8）：1441-1457.

［6］ 龔令侃，王玉艷，章建雄.基于驗(yàn)證庫(kù)的微處理器指令集驗(yàn)證方法［J］.計(jì)算機(jī)工程，2009，35（3）：86-88.

［7］ Guo Qi，Chen Tianshi，Shen Haihua，et al.Empirical Design Bugs Prediction for Verification［C］// Proceedings of Design，Automation&Test in Europe Conference&Exhibition.Washington D.C.，USA：IEEE Press，2011：1-6.

［8］ Kim H，Wills D S，Wills L M.Reducing Operand Communication Overhead Using Instruction Clustering for Multimedia Application［C］//Proceedings of the 7th IEEE International Symposium on Mulitimedia. Washington D.C.，USA：IEEE Press，2005.

［9］ Brahm e D，Abraham J A.Functional Testing of Microprocessors［J］.IEEE Transactions on Com puter，1984，C-33：475-485.

［10］ Salama A E，A li A K，Talkhan E A.Functional Testing of Pipelined Processors［J］.Com puters and Digital Techniques，IEE Proceedings，1996，143（5）：318-324.

［11］ Talkhan A，Ahmed H，Salama E.Microprocessors Functional Testing Techniques［J］.IEEE Transactions on Computer-Aided Design，1989，8（3）：316-319.

［12］ Hennessy J L，Patterson D A.計(jì)算機(jī)體系結(jié)構(gòu)：量化研究方法［M］.賈洪峰，譯.5版，北京：人民郵電出版社，2013.

編輯 金胡考

Digital Signal Processor Verification Based on Instructions

YANG Xiutao，GU Xiaoqiu
（Beijing Institute of Electronics System Engineering，Beijing 100854，China）

To detect faults brought up by related problem during Digital Signal Processor（DSP）design，a method is presented in this paper.It analyzes the architecture of DSP and constructs its Processor Representation Matrix（PRM）. Each block contains instructions that use same function units.Any two instructions in one block are selected to combine an instructions slice.A ll these slices combine the verification instructions sets.To observe the result of instructions，an observe method is presented.A t the end，it cites that these instructions sets can cover all faults due to data relation in theory.A t the same time，it designs a verification instruction generation system to generate instruction set and applies these instructions to DSPC-01 as stimulus.Silicon verification result show s that this method is effective.

verification；Digital Signal Processor（DSP）；data relation；instruction generation；coverage；automatic generation

楊修濤，谷小秋.基于指令的數(shù)字信號(hào)處理器驗(yàn)證［J］.計(jì)算機(jī)工程，2015，41（9）：97-102.

英文引用格式：Yang Xiutao，Gu Xiaoqiu.Digital Signal Processor Verification Based on Instructions［J］.Computer Engineering，2015，41（9）：97-102.

1000-3428（2015）09-0097-06

A

TP302

10.3969/j.issn.1000-3428.2015.09.017

楊修濤（1978-），男，高級(jí)工程師、博士，主研方向：計(jì)算機(jī)輔助設(shè)計(jì)，VLSI/SoC驗(yàn)證，數(shù)據(jù)分析；谷小秋，工程師。

2014-08-14

2014-10-10 E-m ail：xiutaoyang@outlook.com