高性能DSP軟核中DMA控制器的設(shè)計(jì)與驗(yàn)證

鄭 挺，李 勇

（國(guó)防科學(xué)技術(shù)大學(xué) 計(jì)算機(jī)學(xué)院，湖南 長(zhǎng)沙，410073）

0 引 言

銀河飛騰－邁創(chuàng)，簡(jiǎn)稱 “飛騰－邁創(chuàng)”（英文YHFT－Matrix，簡(jiǎn)稱FT－Matrix）是由國(guó)防科大計(jì)算機(jī)學(xué)院微電子與微處理器研究所研發(fā)的具有自主知識(shí)產(chǎn)權(quán)的面向無(wú)線通信、視頻和圖像處理的高性能浮點(diǎn)DSP軟核。數(shù)字信號(hào)處理器（DSP）的主要任務(wù)是完成大量實(shí)時(shí)數(shù)據(jù)計(jì)算，它強(qiáng)大計(jì)算能力的發(fā)揮離不開(kāi)高效的數(shù)據(jù)供給，設(shè)計(jì)一個(gè)可高效搬移數(shù)據(jù)的部件——直接存儲(chǔ)器訪問(wèn)控制器 （DMAC），對(duì)DSP性能的提升具有重要意義。

本文針對(duì)該DSP軟核的應(yīng)用特點(diǎn)，提出了一種靈活高效的DMAC方案。為保證設(shè)計(jì)的正確性，本文用兩種方法對(duì)設(shè)計(jì)進(jìn)行了驗(yàn)證：傳統(tǒng)的模擬驗(yàn)證方法和目前國(guó)內(nèi)外研究熱點(diǎn)之一的基于SVA （system verilog assertion）的驗(yàn)證方法。它們的驗(yàn)證能力互補(bǔ)，將它們結(jié)合起來(lái)驗(yàn)證，可充分發(fā)揮各自的優(yōu)點(diǎn)。

1 IP核體系結(jié)構(gòu)簡(jiǎn)介

YHFT－Matrix內(nèi)核是基于超長(zhǎng)指令字 （very long instruction word，VLIW）的單核與多核動(dòng)態(tài)切換的體系結(jié)構(gòu)并運(yùn)用了單指令流多數(shù)據(jù)流 （single instruction multiple data，SIMD）、單指令流多線程 （single instruction multiple threads，SIMT）技術(shù)，其獨(dú)特的雙指令流多線程 （double instruction multiple threads，DIMT）模式支持操作系統(tǒng)和應(yīng)用算法的同時(shí)運(yùn)行。

IP核的整體結(jié)構(gòu)如圖1所示，該結(jié)構(gòu)主要包括統(tǒng)一的取指、派發(fā)部件、標(biāo)量處理單元、向量處理單元、向量存儲(chǔ)及控制部件、指令緩沖器 （Icache）、數(shù)據(jù)緩沖器（Dcache）及直接存儲(chǔ)器訪問(wèn)控制器 （DMAC）。其中，直接存儲(chǔ)器訪問(wèn)控制器 （DMAC）是DSP的核心數(shù)據(jù)傳輸引擎，它的性能的高低對(duì)芯片的整體性能具有重要影響。

圖1 FT－Matrix IP核總體結(jié)構(gòu)

圖2 DMA控制器的整體結(jié)構(gòu)

2 DMA控制器的設(shè)計(jì)

為滿足以3G／4G無(wú)線通信為代表的高密集度計(jì)算對(duì)數(shù)據(jù)供給的要求，設(shè)計(jì)了兩個(gè)可快速在核內(nèi)外搬移數(shù)據(jù)的通用通道和用于與外部通信的4個(gè)AXI通道。為滿足對(duì)DSP仿真調(diào)試的需要，設(shè)計(jì)一個(gè)與ET （Emulation／Test）部件連接的通道。為加快數(shù)據(jù)的搬移速度，設(shè)計(jì)了多總線、集中式仲裁的結(jié)構(gòu)。

2.1 DMA控制器的整體結(jié)構(gòu)和各通道實(shí)現(xiàn)的功能

DMA控制器的結(jié)構(gòu)如圖2所示。DMA控制器包括通用通道1、通用通道2、AXI（advanced extensible interface）主機(jī)發(fā)送通道、AXI主機(jī)接收通道、AXI從機(jī)發(fā)送通道、AXI從機(jī)接收通道、ET專用通道7個(gè)物理通道和5套總線。

（1）通用通道：可將片外存儲(chǔ)器中的數(shù)據(jù)搬到片內(nèi)存儲(chǔ)器，再將運(yùn)算結(jié)果由片內(nèi)存儲(chǔ)器搬到片外存儲(chǔ)器，同時(shí)可通過(guò)外設(shè)總線實(shí)現(xiàn)各部件參數(shù)的批量配置或讀取。

（2）AXI主機(jī)發(fā)送通道：DMAC作為AXI主機(jī)主動(dòng)從VM、ASRAM （asynchronous RAM）或DDR （double data rate SDRAM）讀取數(shù)據(jù)，并將讀到的數(shù)據(jù)轉(zhuǎn)發(fā)給AXI從機(jī)。

（3）AXI主機(jī)接收通道：DMAC作為AXI主機(jī)主動(dòng)向AXI從機(jī)發(fā)出讀請(qǐng)求，并將從AXI從機(jī)接收到的數(shù)據(jù)寫(xiě)至VM、ASRAM或DDR中。

（4）AXI從機(jī)發(fā)送通道：DMAC作為AXI從機(jī)被動(dòng)接收AXI主機(jī)讀burst信息，并將從VM、ASRAM或DDR讀到的數(shù)據(jù)返回給AXI主機(jī)，本通道在與AXI主機(jī)進(jìn)行burst信息握手成功后，自動(dòng)進(jìn)行數(shù)據(jù)的傳輸，因而需要使用本通道時(shí)，只需要配置AXI主機(jī)方，不需要配置DMAC方。

（5）AXI從機(jī)接收通道：DMAC作為AXI從機(jī)被動(dòng)接收AXI主機(jī)寫(xiě)burst信息，接收AXI主機(jī)寫(xiě)數(shù)據(jù)，并轉(zhuǎn)發(fā)給VM、ASRAM或DDR。本通道與AXI從機(jī)發(fā)送專用通道一樣，在與AXI主機(jī)進(jìn)行burst信息握手成功后，自動(dòng)進(jìn)行數(shù)據(jù)的傳輸，因而需要使用本通道時(shí)，只需要配置AXI主機(jī)方，不需要配置DMAC方。

（6）ET專用通道：用于接收ET部件的請(qǐng)求，并對(duì)存儲(chǔ)空間進(jìn)行讀寫(xiě)操作。若為讀，它將讀到的數(shù)據(jù)返回給ET部件。若為寫(xiě)，它將ET部件的寫(xiě)數(shù)據(jù)寫(xiě)往相應(yīng)部件。

（7）總線仲裁：DMAC可以訪問(wèn)5套總線，分別為DMA總線、VM總線和外設(shè)總線、AXI主機(jī)總線和AXI從機(jī)總線。其中AXI主機(jī)總線和AXI從機(jī)總線為DMA和AXI主機(jī)之間的專用總線，DMA總線主要為EMIF（external memory interface）和ET部件服務(wù)，VM總線為DMAC和VM之間的專用總線，而外設(shè)總線則是DMAC訪問(wèn)片上存儲(chǔ)器映射寄存器空間的通道。

圖3 DMA控制器和其他部件的接口

2.2 DMA控制器參數(shù)化設(shè)計(jì)

IP核的全局地址空間分配方案見(jiàn)表1。其中，ASRAM、VM、I／O空間和DDR的大小均可自己定義，I／O空間又可分配許多小空間。由此導(dǎo)致地址不固定的問(wèn)題，而DMAC是根據(jù)地址向相應(yīng)部件提供數(shù)據(jù)的，因此需要將地址進(jìn)行參數(shù)化處理。

表1 全局地址分配

Verilog HDL語(yǔ)言提供了編譯預(yù)處理命令｀define［1］，宏定義｀define的語(yǔ)法為：｀define宏名 字符串｀define命令可以定義在模塊里，也可定義在模塊外，它的作用范圍為定義命令之后到源文件結(jié)束。

參數(shù)化的DMAC需要定義的參數(shù)有：

｀define ASRAMSpace

｀define VM＿Start＿Addr

｀define VMSpace

｀define ETAddr＿Start

｀define DMAAddr＿Start

｀define DDRAddr＿Start

｀define DDRSpace

2.3 DMA控制器和其它部件的接口

DMA控制器和其它部件的接口如圖3所示。

其中，向量數(shù)據(jù)流重整理緩沖器 （vector rearrange buffer，VRB）是為了解決DMAC （32位）和 VM （512位）之間帶寬不匹配而設(shè)計(jì)的存儲(chǔ)器，大大減少了DMAC訪問(wèn)VM的次數(shù)，使VM可以更好的為向量運(yùn)算單元的數(shù)據(jù)訪問(wèn)操作提供支持，提高了系統(tǒng)性能。DMAC可通過(guò)EMIF訪問(wèn)片外存儲(chǔ)器 （ASRAM和DDR）。

2.4 DMA控制器與外部接口協(xié)議介紹

DMAC的兩個(gè)通用通道和ET專用通道遵循內(nèi)部通信協(xié)議，AXI從機(jī)發(fā)送通道和AXI從機(jī)接收通道遵循標(biāo)準(zhǔn)的AMBA AXI協(xié)議，AXI主機(jī)發(fā)送通道和AXI主機(jī)接收通道遵循簡(jiǎn)化的AMBA AXI協(xié)議。以下僅對(duì)AXI協(xié)議作簡(jiǎn)要介紹。

AXI協(xié)議是ARM公司為適應(yīng)SoC技術(shù)的發(fā)展，面向高性能、高頻率的系統(tǒng)設(shè)計(jì)而適時(shí)推出的的新一代高速總線互連協(xié)議。

AXI協(xié)議［2］是基于突發(fā)傳輸?shù)?，讀寫(xiě)分開(kāi)的通道結(jié)構(gòu)降低了直接存儲(chǔ)器訪問(wèn)的開(kāi)銷。讀通道由讀地址通道和讀數(shù)據(jù)通道構(gòu)成，如圖4所示。寫(xiě)通道由寫(xiě)地址通道、寫(xiě)數(shù)據(jù)通道和寫(xiě)回復(fù)通道構(gòu)成，如圖5所示。這5個(gè)獨(dú)立的通道通過(guò)VALID和READY完成握手，當(dāng)這兩個(gè)信號(hào)同時(shí)為高才開(kāi)始傳輸。

2.5 DMA控制器的特點(diǎn)

DMA控制器主要有如下特點(diǎn)：

（1）后臺(tái)操作：傳輸數(shù)據(jù)的過(guò)程中CPU不參與，提高了系統(tǒng)效率；

（2）多種啟動(dòng)方式：CPU直接啟動(dòng)、外部同步事件啟動(dòng)、通道鏈接啟動(dòng)；

（3）多種同步方式：?jiǎn)卧健⒃磶?、目的幀同步、塊同步；

（4）傳輸數(shù)據(jù)大小靈活：可按字節(jié)、半字、字傳輸；

（5）地址修改方式多樣：源和目的地址可按固定、自增、自減、索引 （有符號(hào)數(shù)）方式修改；

（6）支持二維傳輸：如圖6所示，所需搬運(yùn)的所有數(shù)據(jù)可以分成n幀，每幀幀內(nèi)的數(shù)據(jù)間隔為x（這可以看成第一維），任意緊挨著的兩幀中，前一幀的最后一個(gè)數(shù)據(jù)和后面一幀的第一個(gè)數(shù)據(jù)地址間隔為y（這是第二個(gè)維度）。一般地，所需搬運(yùn)的數(shù)據(jù)有兩種地址間隔，就需要用到二維傳輸；

圖6 二維傳輸

圖7 測(cè)試平臺(tái)的結(jié)構(gòu)

3.1.2 模擬驗(yàn)證驗(yàn)證過(guò)程

驗(yàn)證采用自底向上的驗(yàn)證方法，選用Cadence公司的NC－Verilog模擬器，通過(guò)觀察波形和查看日志文件進(jìn)行驗(yàn)證。驗(yàn)證流程如圖8所示，其中覆蓋率統(tǒng)計(jì)的是代碼覆蓋率。

（7）搬移數(shù)據(jù)能力強(qiáng)：配置一次，最大可搬移 （2n－1）＊2n個(gè)數(shù) （n為計(jì)數(shù)器寬度）。

3 功能驗(yàn)證

功能驗(yàn)證是指證明設(shè)計(jì)實(shí)現(xiàn)的電路模塊的功能和設(shè)計(jì)規(guī)范中規(guī)定的功能是否一致的過(guò)程。在目前的SoC設(shè)計(jì)中，功能驗(yàn)證占整個(gè)設(shè)計(jì)流程的50%～80%，并且隨著SoC規(guī)模和復(fù)雜度的增加，這個(gè)比例還可能增加，功能驗(yàn)證已成為SoC設(shè)計(jì)流程的最大瓶頸。

目前的功能驗(yàn)證方法主要有：模擬驗(yàn)證、形式化驗(yàn)證、基于斷言的半形式化驗(yàn)證、仿真驗(yàn)證、軟硬件協(xié)同仿真驗(yàn)證等。本文只對(duì)模擬驗(yàn)證和基于斷言的驗(yàn)證進(jìn)行研究。

3.1 模擬驗(yàn)證

模擬驗(yàn)證是傳統(tǒng)的驗(yàn)證方法，是動(dòng)態(tài)驗(yàn)證。它的優(yōu)點(diǎn)是簡(jiǎn)單、使用靈活且不受設(shè)計(jì)規(guī)模的限制，目前仍然是主要的功能驗(yàn)證方法。缺點(diǎn)是隨著設(shè)計(jì)規(guī)模的不斷增大和復(fù)雜度的不斷提高，要手工編寫(xiě)的測(cè)試激勵(lì)非常龐大，驗(yàn)證所耗費(fèi)的時(shí)間越來(lái)越難以忍受并且只能證明設(shè)計(jì)有錯(cuò)而不能證明無(wú)錯(cuò)。

3.1.1 測(cè)試平臺(tái)的搭建

測(cè)試平臺(tái) （Testbench）：通常指用來(lái)為設(shè)計(jì)產(chǎn)生特定的輸入序列并觀察響應(yīng)的一段模擬代碼。

測(cè)試平臺(tái)的結(jié)構(gòu)如圖7所示：測(cè)試平臺(tái)為設(shè)計(jì)提供輸入信號(hào)，并監(jiān)視設(shè)計(jì)的輸出信號(hào)。其中輸入激勵(lì)在模塊級(jí)是用硬件描述語(yǔ)言Verilog編寫(xiě)，在系統(tǒng)級(jí)是用匯編語(yǔ)言 （通過(guò)自主研發(fā)的開(kāi)發(fā)環(huán)境將匯編語(yǔ)言轉(zhuǎn)化為機(jī)器碼）編寫(xiě)。

圖8 模擬驗(yàn)證流程

其中，由于4個(gè)AXI通道是為用戶預(yù)留的，可掛載遵循本設(shè)計(jì)協(xié)議的任何AXI設(shè)備，沒(méi)有連接特定的部件，故系統(tǒng)級(jí)的驗(yàn)證成為了一大難點(diǎn)。為在系統(tǒng)級(jí)進(jìn)行驗(yàn)證，我們將DMAC自身的AXI主機(jī)發(fā)送通道和AXI從機(jī)接收通道對(duì)接，AXI主機(jī)接收通道和AXI從機(jī)發(fā)送通道對(duì)接。

在進(jìn)行大批量的數(shù)據(jù)傳輸時(shí)，我們編寫(xiě)了數(shù)據(jù)自動(dòng)比較程序，大大提高了驗(yàn)證效率。

3.1.3 代碼覆蓋率

代碼覆蓋率是一種評(píng)估選取的測(cè)試激勵(lì)好壞和執(zhí)行被測(cè)設(shè)計(jì)程度的方法，也是衡量驗(yàn)證完備性的重要指標(biāo)。它包括塊 （block）覆蓋率、表達(dá)式 （expression）覆蓋率、翻轉(zhuǎn) （toggle）覆蓋率和有限狀態(tài)機(jī) （FSM）覆蓋率。

各覆蓋率的作用如下：

塊覆蓋率：用于監(jiān)視源代碼的語(yǔ)句塊的執(zhí)行情況。

表達(dá)式覆蓋率：用于提供條件表達(dá)式怎樣執(zhí)行的信息。

翻轉(zhuǎn)覆蓋率：用于測(cè)量設(shè)計(jì)活躍性，如未用到的信號(hào)、常量信號(hào)等。

有限狀態(tài)機(jī)覆蓋率：用于監(jiān)視控制邏輯塊的執(zhí)行情況。

由于翻轉(zhuǎn)覆蓋率是度量設(shè)計(jì)活躍性的，與被測(cè)設(shè)計(jì)的功能無(wú)關(guān)，因此不做統(tǒng)計(jì)。

主要模塊的代碼覆蓋率統(tǒng)計(jì)見(jiàn)表2。

表2 代碼覆蓋率

其中，表達(dá)式覆蓋率未達(dá)到100%是由于覆蓋率統(tǒng)計(jì)工具ICC列出的組合不存在。

3.2 基于斷言的驗(yàn)證

斷言是對(duì)設(shè)計(jì)的行為的描述，是一段代碼。

基于斷言的驗(yàn)證方法是半形式化驗(yàn)證方法。半形式化驗(yàn)證方法是一種混合形式驗(yàn)證方法，即模擬和形式驗(yàn)證相結(jié)合。模擬難以對(duì)整個(gè)狀態(tài)空間搜素，形式驗(yàn)證不能處理大的設(shè)計(jì)。把兩者結(jié)合起來(lái)就可以彌補(bǔ)相互的不足之處。

3.2.1 斷言語(yǔ)言選擇

目前，在集成電路設(shè)計(jì)中廣泛使用的斷言語(yǔ)言有：開(kāi)放驗(yàn)證庫(kù)OVL（open verification library）、屬性描述語(yǔ)言PSL（property specification language）、SystemVerilog Assertion （SVA）［3，4］。

OVL是由Accellera組織推出的斷言庫(kù)，這個(gè)庫(kù)是由數(shù)量有限的參數(shù)化的斷言模板組成，用戶只能被動(dòng)地選擇配置參數(shù)來(lái)實(shí)現(xiàn)自己想要的斷言，難以滿足實(shí)際中復(fù)雜多變的應(yīng)用需求［5］。PSL是從IBM開(kāi)發(fā)的Sugar這門(mén)屬性語(yǔ)言演化而來(lái)的一種語(yǔ)言，驗(yàn)證能力雖然強(qiáng)大，但驗(yàn)證人員要使用它必須付出巨大的學(xué)習(xí)開(kāi)銷。

SystemVerilog語(yǔ)言是業(yè)界新興的工程語(yǔ)言，它是對(duì)IEEE Std1364－2001Verilog Standard的一個(gè)擴(kuò)展，其由Accellera標(biāo)準(zhǔn)組織維護(hù)并提交標(biāo)準(zhǔn)化，在2005年12月被標(biāo)準(zhǔn)化為IEEE P1800－2005。它作為統(tǒng)一的設(shè)計(jì)和驗(yàn)證語(yǔ)言，提供強(qiáng)大的面向?qū)ο缶幊碳夹g(shù)，支持約束隨機(jī)的產(chǎn)生，覆蓋率統(tǒng)計(jì)分析和斷言驗(yàn)證，被譽(yù)為下一代芯片設(shè)計(jì)和驗(yàn)證語(yǔ)言［6］。SystemVerilog作為一個(gè)IEEE標(biāo)準(zhǔn)語(yǔ)言，得到了Synopsys、Mentor Graphics和Cadence三大EDA工具提供商的一致支持，已成為設(shè)計(jì)和驗(yàn)證工程師的首選語(yǔ)言［7］。SVA是SystemVerilog語(yǔ)言的子集，能夠滿足驗(yàn)證需要，且簡(jiǎn)單易用，因此，我們選用SVA作為本課題的斷言驗(yàn)證語(yǔ)言。

3.2.2 斷言的優(yōu)缺點(diǎn)

斷言主要有以下優(yōu)點(diǎn)：

（1）復(fù)用性好：傳統(tǒng)驗(yàn)證方法中模塊級(jí)驗(yàn)證和系統(tǒng)級(jí)驗(yàn)證所使用的激勵(lì)是用不同的語(yǔ)言編寫(xiě)的，它們之間無(wú)法重用。而斷言即可用于模塊級(jí)，也可用于系統(tǒng)級(jí)，復(fù)用性好。若斷言是參數(shù)化的，則還可以在不同的項(xiàng)目中復(fù)用。

（2）增加了功能覆蓋率統(tǒng)計(jì)機(jī)制：傳統(tǒng)驗(yàn)證方法的代碼覆蓋率可由覆蓋率統(tǒng)計(jì)工具自動(dòng)完成，功能覆蓋率卻無(wú)法自動(dòng)統(tǒng)計(jì)。而在基于斷言的驗(yàn)證中，覆蓋率可通過(guò)和覆蓋率屬性 （cover property）或覆蓋率組 （covergroup）進(jìn)行描述，當(dāng)斷言被執(zhí)行時(shí)，相應(yīng)的功能就被覆蓋到了。

（3）可縮短驗(yàn)證時(shí)間：Verilog是一種過(guò)程語(yǔ)言，不能很好地描述時(shí)序，而要檢測(cè)時(shí)序，需要編寫(xiě)大量代碼，而用SVA可用很短的代碼實(shí)現(xiàn)，斷言減少了編寫(xiě)代碼的時(shí)間。另外，當(dāng)設(shè)計(jì)有錯(cuò)誤時(shí)，得花大量時(shí)間追溯錯(cuò)誤發(fā)生的位置，而在基于斷言的驗(yàn)證中，一旦斷言監(jiān)測(cè)到錯(cuò)誤，工具就會(huì)報(bào)出出錯(cuò)的具體位置，大大節(jié)省了調(diào)試時(shí)間。

SystemVerilog斷言 （SVA）雖可以完美的描述和控制與時(shí)序相關(guān)的問(wèn)題，但卻不適用于檢測(cè)數(shù)據(jù)轉(zhuǎn)換、計(jì)算和順序錯(cuò)誤［8］。

3.2.3 SVA的分類

SystemVerilog語(yǔ)言定義了兩種斷言：即時(shí)斷言 （immediate assertions）和并發(fā)斷言 （concurrent assertions）。

（1）即時(shí)斷言：即時(shí)斷言是基于模擬事件的語(yǔ)義，必須放在過(guò)程塊的定義中，它們本質(zhì)不是時(shí)序相關(guān)的，測(cè)試表達(dá)式被立即求值且只能用于動(dòng)態(tài)模擬。

一個(gè)即時(shí)斷言的例子如下：

always＿comb

begin

a1：assert（a｜b）；

end

（2）并發(fā)斷言：并發(fā)斷言是基于時(shí)鐘周期的，可以放到過(guò)程塊（procedural）、 模塊（module）、接口（interface），或者一個(gè)程序（program）的定義中［9］，在時(shí)鐘邊沿根據(jù)調(diào)用的變量的采樣值計(jì)算測(cè)試表達(dá)式且可以在靜態(tài)（形式的）驗(yàn)證和動(dòng)態(tài)驗(yàn)證 （模擬）工具中使用。

一個(gè)并發(fā)斷言的例子如下：

a2：assert property （＠ （posedge clk）a｜－＞b）；

區(qū)別即時(shí)斷言和并發(fā)斷言的關(guān)鍵詞是 “property”。在驗(yàn)證過(guò)程中，大多使用并發(fā)斷言，即時(shí)斷言很少使用。

3.2.4 基于斷言的驗(yàn)證過(guò)程

SVA包含assume、assert和cover這3個(gè)指令［10］。其中assume用于對(duì)環(huán)境進(jìn)行假定，形式化工具用它來(lái)產(chǎn)生帶約束的激勵(lì)；assert用于監(jiān)視它描述的設(shè)計(jì)的屬性；cover用于監(jiān)視覆蓋率屬性。SVA可以嵌入到設(shè)計(jì)代碼中，也可放在單獨(dú)的文件中。

我們選用Mentor Graphics公司的形式化驗(yàn)證工具Questa Formal進(jìn)行驗(yàn)證，在驗(yàn)證之前，估測(cè)待測(cè)設(shè)計(jì)的規(guī)模完全在工具高效運(yùn)行的范圍 （25萬(wàn)門(mén)）之內(nèi)?；跀嘌缘尿?yàn)證流程如圖9所示，我們采用 “灰盒”的驗(yàn)證方法，重點(diǎn)對(duì)控制邏輯、接口協(xié)議和總線仲裁進(jìn)行了驗(yàn)證。

圖9 基于斷言的驗(yàn)證流程

3.2.5 驗(yàn)證結(jié)果

在驗(yàn)證過(guò)程中發(fā)現(xiàn)了一個(gè)功能缺陷和一個(gè)語(yǔ)法錯(cuò)誤，對(duì)設(shè)計(jì)進(jìn)行修改后，重新進(jìn)行了驗(yàn)證，未發(fā)現(xiàn)新錯(cuò)誤，達(dá)到了預(yù)期目標(biāo)。

Questa Formal軟件最終統(tǒng)計(jì)的斷言屬性檢查結(jié)果如圖10所示。

圖10 斷言屬性檢查結(jié)果

4 性能分析

DMAC的數(shù)據(jù)傳輸速率統(tǒng)計(jì)如表3所示，結(jié)果表明設(shè)計(jì)的DMAC完全能夠滿足內(nèi)核運(yùn)算的需要。

表3 DMAC傳輸速率統(tǒng)計(jì)

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

本課題是在國(guó)家 “核高基”重大專項(xiàng)基金的支持下完成的。本文針對(duì)應(yīng)用需求設(shè)計(jì)了可高效搬移數(shù)據(jù)的部件——DMA控制器，除對(duì)傳統(tǒng)的模擬驗(yàn)證方法進(jìn)行研究外，還重點(diǎn)對(duì)先進(jìn)的基于斷言的功能驗(yàn)證方法進(jìn)行了研究。

傳統(tǒng)的模擬驗(yàn)證方法目前仍是功能驗(yàn)證的主要方法，它能在設(shè)計(jì)的前期和早期發(fā)現(xiàn)大量和明顯的錯(cuò)誤，但隨著設(shè)計(jì)規(guī)模的增大和復(fù)雜度的提高，已經(jīng)越來(lái)越不能滿足驗(yàn)證需求。

基于斷言的驗(yàn)證方法與傳統(tǒng)的驗(yàn)證方法相比，復(fù)用性好，增加了功能覆蓋率統(tǒng)計(jì)機(jī)制，可縮短驗(yàn)證時(shí)間，并且能夠發(fā)現(xiàn)傳統(tǒng)驗(yàn)證方法無(wú)法發(fā)現(xiàn)的錯(cuò)誤，提高驗(yàn)證質(zhì)量。其缺點(diǎn)是能夠驗(yàn)證的設(shè)計(jì)規(guī)模有限，得與模擬驗(yàn)證方法結(jié)合使用。

［1］XIA Yuwen.Digital system design tutorial for verilog ［M］.2nd ed.Beijing：Beijing University of Aeronautics and Astronautics Press，2008：106－107 （in Chinese）.［夏宇聞.Verilog數(shù)字系統(tǒng)設(shè)計(jì)教程 ［M］.2版.北京：北京航空航天大學(xué)出版社，2008：106－107.］

［2］ARM IHI 0022D，AMBA AXITMand ACETMprotocol specification ［S］.2011.

［3］LIANG Lihua.Assertion－based verifieation researeh and Application ［D］.Dalian：Dalian Maritime University，2008：11－12（in Chinese）.［梁麗華.基于斷言的功能驗(yàn)證方法研究及其應(yīng)用 ［D］.大連：大連海事大學(xué)，2008：11－12.］

［4］LIU Xuheng.The research of system verilog assertion－based verification method for nand flash controller［D］.Hefei：Anhui University，2011 （in Chinese）.［劉旭恒.基于SVA的 NFC驗(yàn)證方法研究 ［D］.合肥：安徽大學(xué)，2011.］

［5］Software Version 2.6，Accellera standard OVL V2library refe－rence manual［S］.2011.

［6］ZHONG Wenfeng.Design and verification language of next generation chip：SystemVerilog （verification）［DB］.http：／／www.cnki.net，2008 （in Chinese）.［鐘文楓.下一代芯片設(shè)計(jì)與驗(yàn)證語(yǔ)言：SystemVerilog （驗(yàn)證篇）［DB］.http：／／www.cnki.net，2008.］

［7］ZHONG Wenfeng.SystemVerilog and functional verification［M］.Beijing：China Machine Press，2010：20－35 （in Chinese）.［鐘文楓.SystemVerilog與功能驗(yàn)證 ［M］.北京：機(jī)械工業(yè)出版社，2010：20－35.］

［8］Janick Bergeron，Eduard Cerny，Alan Hunter，et al.Verification methodology manual for SystemVerilog［M］.XIA Yuwen，YANG Lei，CHEN Xianyong，et al transl.Beijing：Beijing University of Aeronautics and Astronautics Press，2007：27－85 （in Chinese）.［Janick Bergeron，Eduard Cerny，Alan Hunter.SystemVerilog驗(yàn)證方法學(xué) ［M］.夏宇聞，楊雷，陳先勇，等譯.北京：北京航空航天大學(xué)出版社，2007：27－85.］

［9］CHENG Gang.Research of functional verification based on system verilog ［D］.Guangzhou：South China University，2010：28－29（in Chinese）.［程剛.基于System Verilog的功能驗(yàn)證方法研究 ［D］.廣州：華南理工大學(xué)，2010：28－29.］

［10］IEEE Std 1800TM－2009，IEEE Standard for SystemVerilog－unified hardware design，specification，and verification language［S］.2009.