基于指令的数字信号处理器验证

杨修涛，谷小秋

（北京电子工程总体研究所，北京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