基于指令的數字信號處理器驗證

楊修濤，谷小秋

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

基于指令的數字信號處理器驗證

楊修濤，谷小秋

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

針對數字信號處理器設計中因相關引發的故障，提出一種基于指令的驗證方法。結合處理器的體系結構特點給出處理器表示矩陣，并利用該矩陣，根據所使用的功能單元對指令進行劃分。在同一個劃分內，指令使用相同的功能單元，對這些指令進行兩兩組合，生成驗證指令序列?？紤]測試的可觀測性給出觀測方法，從理論上證明該方法可以完備覆蓋到所有數據相關故障。設計驗證指令生成系統自動生成驗證指令序列，針對DSPC-01處理器進行實驗，并與流片后的測試結果比較分析，結果驗證了該方法的有效性。

驗證；數字信號處理器；數據相關；指令生成；覆蓋率；自動生成

1 概述

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

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

2 相關工作

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

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

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

表1 PRM元素含義

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

表2 ADD指令的PRM表示

DSPC-01處理器與一般通用處理器有些不同，它有2個計算塊。因此，分別有2個ALU及相關寄存器堆，表現在表2上就是ALU 1對應著寄存器堆XR及操作M1，ALU2對應寄存器堆YR及操作M1。在后面中，所有類同的指令均會有相同的表現。在此基礎上，本文給出DSPC-01的PRM構造方法。

2.1 DSPC-01處理器及指令集

DSPC-01是一個具有128位數據總線，支持超長指令字（Very Long Instruction Word，VLIW）的超標量數字信號處理器。分別對稱地擁有2個ALU（ALU1，ALU2）、2個移位器（SHF1，SHF2）、3個2 MB的寄存器堆（一個為指令寄存器堆，另兩個分別為XR和YR）、2個乘法器（MUL1，MUL2）以及2個整數ALU（IALU1，IALU2）。

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

需要說明的是，在DSPC-01的具體實現中CLU指令是在ALU中進行執行的，所以，這兩部分指令可以統一劃歸于ALU中。對于IALU，它同ALU一樣，也是有2個計算塊，所不同的是在IALU中，它分為XI和Y I計算塊，而對應的其計算塊中的寄存器堆也變成X IR0～X IR15，YIR0～Y IR15。這樣，可以考慮將XI和YI兩塊分開來分析。部分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個ALU單元，MUL1～MUL2為2個乘法單元。SHIFTER1～2為2個移位器單元，X IR/Y IR分別為IALU1/IALU2中寄存器堆。RAM為M emory，SFR為條件寄存器SFREG。

2.2 DSPC-01的PRM及指令劃分

根據表3和功能單元可以構造出DSPC-01的PRM，該PRM的行剛好由表3中的所有指令組成，而列則由所有功能單元組成。由此，可以得到一個N（指令數）×M（功能單元數）矩陣。在此基礎上，下面給出等價寄存器與等價寄存器集的概念。

定義3 等價寄存器

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

定義4 等價寄存器集

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

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

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

如無特別說明，當某條指令用到某一等價寄存器時，使用等價寄器集來代替。

3 指令自動生成算法

3.1 分類算法

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

同一劃分內的任意2條指令，它們使用完全相同的寄存器集，如果2條指令在流水中相鄰出現，必定會引起數據相關。因此，可以依據這樣的劃分，在每一個劃分內，對所有的指令作組合。如果，將存在數據相關關系的2條指令用一條邊連接，指令作為一個節點，那么，一個劃分內的所有指令組成一個完全圖。依序遍歷所有的邊，可以得到數據相關的驗證指令集，當然該集是針對該劃分內所有指令的共同寄存器的。對所有的劃分進行上述工作可以得到整個指令集內所有劃分的驗證指令集。

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

3.2 指令生成

3.2.1 一拍相關的測試指令生成

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

圖1 由4條指令構成的完全圖

任意2條指令i，j，i與j之間存在數據相關的關系，所以，應該存在一條有向邊i→j，同樣，j與i之間也存在數據相關的關系，所以，亦存在有向邊j→i。就是說，實際上是i，j之間存在2條有向邊。因此，在圖1中可以化簡為無向邊。遍歷這些邊，顯然可以得到指令之間的數據相關關系。比如，遍歷i，j可以得到有向邊i→j；遍歷j，i可以得到j→i。圖1所示的完全圖實際上是遍歷每條邊2次。不妨假設這4個節點分別被標記為i1，i2，i3，i4，那么會有下列遍歷情況：

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

指令在流水線中執行的情形如圖2所示，其中，虛線表示需要補充的一種指令組合關系。

圖2 指令在流水線中被執行示例

將式（3）與式（1）、式（2）對比可知，實際上在一次的遍歷中已覆蓋了大部分相關情況，只需要再補充一個相關關系i4→i1即可。因此，沒有必要遍歷2次。整個的測試生成的算法描述如下：

算法 指令生成

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

輸出 Sc

3.2.2 多拍相關的驗證指令生成

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

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

3.3 可觀測性分析

考慮可觀測性時，可測性設計（Design For Testability，DFT）還不可用，所以，使用DFT以外的方法來實現觀測驗證結果的目的。在實際應用中是借用了DSP的3個靜態存儲器（Static Random Access M emory，SRAM）中的一個來暫存指令運行結果。

由于在驗證過程中，指令需要存儲在指令RAM中，因此只能選擇2個數據RAM來存儲指令運行結果，如圖3所示，其中一個存放的是指令運行過程中需要用到的數據，比如數據存儲器RAM_A，所以選擇另外一個數據存儲器RAM_B來存儲運行的結果。在指令運行完后，將結果從RAM_B中導出進行比對，以觀測指令執行的結果。對于兩拍以上相關的指令，由于中間可以插NOP，因此使用的是插入額外的其他指令來觀測運行結果。所以，對其觀測更容易。

圖3 DSP中的3塊RAM

4 實驗及結果分析

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

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

進一步分析：對于任一可能的單拍數據相關，上述方法是否都能生成一個指令組合以覆蓋到該數據相關。

命題 對于任一由2條相鄰指令所形成的數據相關，上述方法總能給出一個指令組合以覆蓋到該相關關系。

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

如果它們不滿足條件（1），那么它們在同一劃分中，即：Sij=SiK，這樣在同一劃分中一定會有組合ij→iK和iK→ij能覆蓋到該相關關系。因此，它一定滿足條件（1），所以有Rij≠RiK。

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

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

證畢。

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

表4 各模塊驗證結果

由3.3節的可觀測性分析中可知，表4中的數據是在指令序列全部運行完后統計出的。同一個bug可能會被統計到多次，所以，需要在回歸驗證過程中進行篩選。最終回歸驗證收斂后統計出的bug數（非重復）結果如表5所示。

表5 最終驗證檢測到的實際bug個數

將表4、表5的結果進行比較，如圖4所示?？梢钥闯?，表4、表5的bug數量趨勢一致，基本上最初報出bug較多的模塊，實際bug也較多。在實際驗證過程中針對最初報出bug較多的模塊有必要加強驗證。

圖4 bug個數對比

在芯片流片后，針對相應的芯片進行進一步的測試分析，測試過程中，除了使用上述的指令集外，還引入一些實際的Benchmark以及大量的實際應用來對DSPC-01進行測試，檢驗本文方法是否有效。表6給出了部分用例。

表6 成片測試結果

為了進一步檢驗效果，在DSPC-01的驗證過程中，采用先用其他驗證方法驗證，然后用本文方法檢驗的策略。如果本文方法生成的驗證指令集能在已驗證過的模塊上繼續發現bug，那么也能證明本文方法針對驗證是有效的，結果如表7所示。

表7 本文方法結果

可以看到，用B.asm和C.asm共繼續檢測到4個未被發現的bug，經過2個版本的實驗結果比較，證明本方法針對驗證是有效的。

總體上看，該方法是實現了對處理器的功能驗證。對于有RTL代碼的自主設計以及第三方IP核均可達到驗證功能的目的。

5 結束語

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

在未來的工作中，將進一步研究針對網表級的驗證，研究在等價寄存器這一概念不再成立時的驗證指令集生成方法，并加強可觀測性分析和設計，從而做到隨時觀測指令運行結果，便于及時分析、查找設計錯誤。同時對所有的指令模式進行等價性分析及合并，以便能生成更為簡短的驗證指令集。

［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］ 龔令侃，王玉艷，章建雄.基于驗證庫的微處理器指令集驗證方法［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.計算機體系結構：量化研究方法［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

楊修濤，谷小秋.基于指令的數字信號處理器驗證［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-），男，高級工程師、博士，主研方向：計算機輔助設計，VLSI/SoC驗證，數據分析；谷小秋，工程師。

2014-08-14

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