劉 婧，王天成，王 健，3，李華偉

（1.湘潭大學(xué)信息工程學(xué)院，湖南 湘潭411105；2.中國科學(xué)院計算技術(shù)研究所計算機體系結(jié)構(gòu)國家重點實驗室，北京100190；3.中國科學(xué)院大學(xué)，北京100049）

基于指令模板的通用處理器約束隨機指令生成方法

劉 婧1，王天成2，王 健2，3，李華偉2

（1.湘潭大學(xué)信息工程學(xué)院，湖南 湘潭411105；2.中國科學(xué)院計算技術(shù)研究所計算機體系結(jié)構(gòu)國家重點實驗室，北京100190；3.中國科學(xué)院大學(xué)，北京100049）

隨著集成電路設(shè)計的復(fù)雜度越來越高，功能驗證成為設(shè)計流程中的瓶頸。而通用處理器是集成電路中功能最為復(fù)雜的設(shè)計之一，對其功能驗證提出更高要求。為此，給出一種約束隨機指令生成方法，對ARM v8處理器進行模擬驗證。從指令集中提取指令模板，用指令模板生成合法的ARM v8指令，通過調(diào)整約束支持各種功能場景的驗證?；诮Y(jié)果自動比對的驗證環(huán)境，對處理器進行充分驗證，發(fā)現(xiàn)58處設(shè)計錯誤，可用在后續(xù)的FPGA硬件仿真中。驗證結(jié)果表明，該方法可得到90%的結(jié)構(gòu)覆蓋率。

功能驗證；通用處理器；指令模板；指令生成；約束隨機指令

DO I：10.3969/j.issn.1000-3428.2015.10.058

1 概述

隨著現(xiàn)代集成電路工藝的不斷發(fā)展，芯片規(guī)模越來越大，復(fù)雜度越來越高。特別是在通用處理器領(lǐng)域，處理器的設(shè)計日趨復(fù)雜，功能驗證已經(jīng)成為設(shè)計流程中的瓶頸［1］。目前常用的功能驗證方法有模擬驗證和形式化驗證。模擬驗證通過生成驗證激勵分別施加于處理器設(shè)計和參考模型，通過將得到的模擬結(jié)果與參考結(jié)果進行對比，從而發(fā)現(xiàn)設(shè)計錯誤。形式化驗證通過數(shù)學(xué)的方法證明被驗證系統(tǒng)滿足設(shè)計規(guī)范。形式化驗證存在狀態(tài)空間爆炸的問題只能處理較小的設(shè)計規(guī)模［2］，現(xiàn)在工業(yè)界主流的功能驗證方法還是模擬驗證。

對于模擬驗證，得到高效的測試激勵成為研究熱

點。國內(nèi)外很多研究機構(gòu)也都在這個方面提出了眾多的解決方法并開發(fā)相應(yīng)的工具［3］。IBM HAIFA研究中心研發(fā)的Genesys-Pro［4］，為基于模型的隨機程序生成器。加州大學(xué)歐文分校的學(xué)者提出一種體系結(jié)構(gòu)描述語言驅(qū)動的驗證激勵生成方法［5］，該方法針對流水線處理器的驗證。中國科學(xué)院計算技術(shù)研究所龍芯驗證組提出了一種可配置隨機測試程序生成器（Configurable Random test Program Generator，CRPG）［6］，它包含配置規(guī)范模型、參考指令集仿真器測試生成模型以及驗證環(huán)境4個基本組件。國防科技大學(xué)提出了一種由體系結(jié)構(gòu)描述驅(qū)動的基于約束求解的微處理器體系結(jié)構(gòu)級測試程序自動生成的方法，并基于此開發(fā)了原型系統(tǒng)——MA2TG［7］。對于難達狀態(tài)的覆蓋，中國科學(xué)院計算技術(shù)研究所集成電路實驗室研究了半形式化驗證方法。先后提出了通過路徑約束引導(dǎo)驗證激勵生成到達難達狀態(tài)的方法［8］和通過抽象引導(dǎo)生成驗證激勵到達難達狀態(tài)的方法［9］。

本文提出一種基于指令模板的通用處理器約束隨機指令生成方法。該方法基于ARM v8指令集構(gòu)建指令模板，編寫合法性約束，指導(dǎo)生成合法的指令序列。在此基礎(chǔ)上通過約束的調(diào)整可以生成針對特定場景的指令序列。

2 ARM v8處理器

本文驗證的對象為一款基于ARM v8指令集的通用處理器核的設(shè)計，其結(jié)構(gòu)如圖1所示。

圖1 ARM v8整體結(jié)構(gòu)

該處理器特性如下：

（1）處理器采用12級流水結(jié)構(gòu)。

（2）處理器支持四線程。

（3）處理器主要部件包括取指單元（IFU）、Instruction Buff（IB）、取指分發(fā)單元（IFU）、指令譯碼單元（DC）、運算邏輯單元（ALU）、浮點運算單元（FPU）、存儲單元（LSU）。

（4）處理器包含4個通用寄存器堆和浮點寄存器堆，對應(yīng)4個線程。

（5）處理器采用32位簡單指令集結(jié)構(gòu)，共支持指令220條。

（6）處理器集成了16 KB一級I-Cache和16 KB一級D-Cache，同時通過interface連接128 KB二級Cache。

如上所述，待驗證處理器結(jié)構(gòu)復(fù)雜，指令集龐大，即驗證向量空間大，使得用手寫激勵覆蓋所有的功能點實現(xiàn)困難。本文提取處理器功能點，采用約束隨機的方法自動生成大量的合法指令覆蓋這些功能點的方法對待驗證處理器進行驗證。

3 指令生成方法和實現(xiàn)

3.1 驗證框架

本文提出一種基于指令模板的約束隨機指令生成方法，并使用System Verilog語言實現(xiàn)了指令生成平臺。采用模擬驗證的方法，搭建驗證平臺對一款A(yù)RM v8處理器進行了驗證。整個驗證框架結(jié)構(gòu)如圖2所示。

圖2 約束隨機指令生成的驗證框架

通過指令生成得到的驗證激勵分別施加于處理器核設(shè)計和參考模型，然后將得到的模擬結(jié)果和參考結(jié)果進行對比，以判斷處理器核的行為是否正確。同時分析模擬過程中的覆蓋率信息，根據(jù)覆蓋率反饋的驗證漏洞來創(chuàng)建新的驗證場景，以生成新的驗證激勵提高驗證覆蓋率，加速驗證的收斂。

3.2 指令模板

因為用于驗證的指令必須符合ARM v8指令語法結(jié)構(gòu)，所以本平臺構(gòu)建了能指導(dǎo)生成合法指令的指令模板，用于指導(dǎo)生成合法的指令。一條ARM v8匯編指令可能包含的各字段如圖3所示。

圖3 ARM v8指令各字段

在圖3中，opcode為操作碼，cond為條件碼，dst0、dst1分別為第0號、第1號目的寄存器號，scr0、scr1分別為第0號、第1號源寄存器號，immd為立即數(shù)。

為了構(gòu)建指令模板，本文對DUV已實現(xiàn)的所有ARM v8指令進行了分類。為了在驗證過程中能控制驗證的方向，在指令分類時有必要考慮到指令的功能。同時為了使指令模板的構(gòu)建工作盡量簡單，指令語法格式接近的指令，即圖3中各字段內(nèi)容及數(shù)量接近的指令也應(yīng)歸為一類。根據(jù)這2個標(biāo)準(zhǔn)本文最終對指令的分類情況如表1所示［10］。

表1 ARM v8指令分類

根據(jù)每類指令的特點約束其各字段在合法的范圍內(nèi)，拼接各字段成一條合法指令后輸出［11］。對于每類指令都有的共性，定義了BaseInstruction類。其他各類指令對BaseInstruction類進行擴展，實現(xiàn)其特有的屬性。圖4為指令模板指導(dǎo)Load/Store Single Register類指令生成的過程［12］。

圖4 指令模板指導(dǎo)Load/Store Single Register類指令生成

在BaseInstruction中確定可能用到的4個寄存器的編號，可選范圍均為［0：31］。然后進入子類，Load/Single Register子類特有屬性包括：

（1）目的寄存器數(shù)目，該子類只有一個目的寄存器。

（2）該類獨有的操作碼，可選范圍為0～8，不同

的操作碼隱含了傳輸字寬，由此可確定目的寄存器的位寬，32位及以下的數(shù)據(jù)的存儲目的寄存器表示為W d，64位數(shù)據(jù)的存儲目的寄存器表示為Xd。

（3）尋址方式，該類指令根據(jù)不同的尋址方式使用不同的源寄存器，當(dāng)尋址方式是1時，基址寄存器（即源寄存器）為64位寄存器，偏移值為可擴充的12位無符號立即數(shù)或9位不可擴充的有符號立即數(shù)。當(dāng)尋址方式是6時，基址寄存器為PC，偏移地址為19位有符號立即數(shù)，尋址范圍為程序存儲范圍。

3.3 各功能場景下的指令生成

在生成指令前，在指令類層次上可對最終生成的指令序列中各指令類所占比例進行配置。在指令級層次上，可根據(jù)操作碼的不同，對每條指令在本類指令中所占比例進行配置。也可根據(jù)驗證重點的不同生成指令序列觸發(fā)相應(yīng)的功能場景，下文對本平臺實現(xiàn)的幾個重要的功能場景進行介紹。

3.3.1 數(shù)據(jù)相關(guān)指令生成

DUV采用12級流水結(jié)構(gòu)，為了驗證DUV在流水線存在資源讀寫沖突的情況下的行為是否符合設(shè)計規(guī)范的約定，本平臺隨機生成存在寄存器相關(guān)的指令序列以激活這一場景，以驗證DUV的正確性。

數(shù)據(jù)相關(guān)指令生成方法需要完成下列任務(wù)：

（1）考慮到所有的相關(guān)模式。本指令的每個寄存器與其他指令的寄存器之間的相關(guān)性共有3種情況，本指令的寄存器與目標(biāo)指令的源寄存器相關(guān)，本指令的寄存器與目標(biāo)指令的目的寄存器相關(guān)，本指令與目標(biāo)指令不存在寄存器相關(guān)。本指令的寄存器分為源寄存器和目的寄存器。當(dāng)存在相關(guān)性時還分為與第0號和第1號寄存器相關(guān)2種情況。

（2）指定相關(guān)深度，2條存在相關(guān)性的指令之間的最大跨度，根據(jù)DUV流水線深度確定。

（3）能實現(xiàn)相關(guān)模式各類情況概率的可控性。

數(shù)據(jù)相關(guān)指令生成方法的關(guān)鍵在于編寫合法性約束以及維護歷史使用寄存器隊列。在生成指令序列前，合法性約束能實現(xiàn)根據(jù)不同的驗證要求對指令間相關(guān)性種類、各相關(guān)性種類的概率進行配置。

生成數(shù)據(jù)相關(guān)指令的寄存器編號通過如下所示的程序偽碼得到：

foreach reg

//不存在相關(guān)性或相關(guān)深度所指記錄無效則該寄存器編//號為隨機值

if c-m-sel==‵N||hist-q.regs［c-d］.f==0；gen-reg-num=reg-num；//查詢歷史寄存器隊列else

gen-reg-num=hist-q.regs［c-d］.c-m-sel；

hist-q.regs.push-front（regs-info）；

hist-q.regs.pop-back；

在生成指令時對于指令中的各寄存器，如果不存在相關(guān)性或者相關(guān)深度（c-d）所指的記錄中有效性標(biāo)志f為 0，則寄存器編號為 0～31的一個隨機值reg-num，否則，寄存器編號為歷史使用寄存器隊列（hist-q）中相關(guān)深度、相關(guān)模式（c-m-sel）所指的寄存器的編號。最后把本條指令使用到的寄存器信息reg-info壓入到hist-q隊頭。hist-q中的每條記錄regs-info包括7個元素｛f，dest-cnt，scr-cnt，dest-0，dest-1，scr-0，scr-1｝，它們分別代表此條記錄的有效性、目的寄存器數(shù)目、源寄存器數(shù)目、第0個目的寄存器的寄存器號、第1個目的寄存器的寄存器號、第0個源寄存器的寄存器號、第1個源寄存器的寄存器號。3.3.2 跳轉(zhuǎn)指令生成

跳轉(zhuǎn)指令關(guān)系到處理器轉(zhuǎn)移預(yù)測、跳轉(zhuǎn)預(yù)判、流水線等功能的實現(xiàn)是否符合要求。所以本文搭建的指令生成平臺對跳轉(zhuǎn)指令進行了重點驗證。

生成跳轉(zhuǎn)指令時很容易生成非法指令，為了生成合法指令，需要注意以下3點：

（1）每類跳轉(zhuǎn)指令的跳轉(zhuǎn)范圍是一定的，所以在生成指令時要添加約束保證跳轉(zhuǎn)范圍的合法性。

（2）因為生成的指令序列是一定的，所以跳轉(zhuǎn)所指向的目標(biāo)地址應(yīng)該存儲了指令，需要添加約束使得跳轉(zhuǎn)的范圍在生成的指令序列范圍內(nèi)。

（3）跳轉(zhuǎn)指令目標(biāo)地址不能是綁定為一個指令包的中間指令，如要實現(xiàn)帶寄存器的跳轉(zhuǎn)指令（BR）要先向寄存器中寫入跳轉(zhuǎn)目標(biāo)地址。本文用2條指令（mov、movk）完成寫目標(biāo)地址的寫操作。因此BR指令的功能由這2條寫地址指令后跟著實際的跳轉(zhuǎn)指令（br）組成的指令包來完成。顯然當(dāng)其他跳轉(zhuǎn)指令的目標(biāo)地址指向該指令包的后2條指令時會發(fā)生錯誤。為了解決這個問題，本指令生成平臺對生成的指令數(shù)進行計數(shù)，然后將跳轉(zhuǎn)指令的目標(biāo)地址和指令包起始地址都放置在指令序號模3為1的位置。

3.3.3 Load Forward指令生成

指令生成流程如圖5所示。

圖5 load forward指令生成流程

在訪存指令中，如果 Load指令要取的數(shù)據(jù)在Store Buffer中，則直接從store buffer中forward到寄存器，而不訪問內(nèi)存。為了驗證DUV在滿足條件的情況下是否能成功實現(xiàn)forward功能，以及在條件不成立的情況下是否會出現(xiàn)forward紊亂，本文提出了一種控制激活load forward的方法：維護一個store指令（str-ins）歷史訪問地址隊列（q-fwd）來存儲str-ins歷史訪問的內(nèi)存地址（mem-addr）。q-fwd共存儲了指定條數(shù)（根據(jù)Store Buffer的長度而定）記錄。

首先對load forward與q-fwd中各記錄的相關(guān)概率進行配置，然后開始生成指令。若當(dāng)前指令為str-ins則將mem-addr壓入q-fwd隊頭，q-fwd隊尾元素彈出，否則為load指令。若此load指令不激活load forward，此指令的mem-addr為隨機值，否則mem-addr為q-fwd中相應(yīng)記錄，然后根據(jù)指令訪存數(shù)據(jù)寬度對mem-addr進行對齊處理，此mem-addr拼接上指令其他字段，指令生成完成。

因為存儲一致性的驗證比較復(fù)雜，本平臺對于四線程的驗證采用生成4個指令序列，存儲在互不重疊的內(nèi)存單元以供給4個相應(yīng)的線程的方式進行驗證。

4 驗證效果與分析

本文針對前述一款A(yù)RM v8處理器，搭建了指令生成平臺和驗證平臺對其進行驗證。在驗證過程中，通過分析每個階段的覆蓋率報告，對該階段未能覆蓋到的功能，本平臺采取添加約束，引導(dǎo)指令生成平臺生成能激活這些功能的指令以達到提高覆蓋，加速驗證收斂的目的。在驗證工作結(jié)束時，約束隨機指令要求覆蓋到的功能點全部覆蓋到，即功能覆蓋率達到100%。結(jié)構(gòu)覆蓋率達到了90%，對覆蓋率進行分析后，發(fā)現(xiàn)關(guān)于中斷與異常處理的模塊未能覆蓋到，而這些模塊不通過隨機約束指令來進行驗證，所以采取定向激勵來對其進行驗證，使得結(jié)構(gòu)覆蓋率達到了100%。本平臺在約束隨機驗證過程中幫助設(shè)計人員發(fā)現(xiàn)了58處設(shè)計錯誤，根據(jù)功能單元的不同，下面對錯誤出處進行了分類，如圖6所示。

圖6 各單元bug數(shù)

本文以每周發(fā)現(xiàn)錯誤為單位，對設(shè)計錯誤數(shù)進行了統(tǒng)計，如圖7所示。從圖中曲線趨勢可以看出，隨著驗證過程的持續(xù)深入和時間的推移，錯誤數(shù)逐漸收斂。此后將有信心將驗證的過程從模擬驗證過度到后續(xù)的FPGA硬件仿真和原型驗證，進行更大規(guī)模和更快速度的集成驗證。

圖7 每周發(fā)現(xiàn)的bug數(shù)

5 結(jié)束語

本文提出了一種基于指令模板的隨機指令生成方法，搭建了指令生成平臺并利用其對一款A(yù)RM v8處理器進行了驗證。該指令生成平臺具有較強的靈活性和易操作性。最終取得了結(jié)構(gòu)覆蓋率90%、發(fā)現(xiàn)設(shè)計錯誤58處的驗證效果，為處理器進入后續(xù)的FPGA硬件仿真奠定了良好的基礎(chǔ)。

［1］ ITRS.ITRS2008［EB/OL］.（2008-02-08）.http：//pub lic.itrs.net/.

［2］ 李曉維.集成電路設(shè)計驗證［M］.北京：科學(xué)出版社，2010.

［3］ 沈海華.覆蓋率驅(qū)動的隨機測試生成技術(shù)綜述［J］.計算機輔助設(shè)計與圖形學(xué)學(xué)報，2009，21（4）：419-430.

［4］ Adir A.，Almog E，F(xiàn)ournler L，et al.Genesys-Pro：Innovations in Test Program Generation for Functional Processor Verification［J］.IEEE Design&Test of Computers，2004，21（2）：84-93.

［5］ Mishra P，Dutt N.Graph-based Functional Test Program Generation for Pipelined Processors［C］//Proceedings of Design Automation and Test in Europe Conference. Paris，F(xiàn)rance：［s.n.］，2004：182-187.

［6］ Shen H H，CRPG：A Configurable Random Test-program Generator for Microprocessors［C］//Proceedings of IEEE International Symposium on Circuits and Systems. Washington D.C.，USA：IEEE Press，2005：4171-4174.

［7］ 朱 丹.微處理器體系結(jié)構(gòu)級測試程序自動生成技術(shù)［J］.軟件學(xué)報，2005，16（12）：2172-2180.

［8］ Zhou Yanhong，Wang Tiancheng.Path Constraint Solving Based Test Generation for Hard-to-Reach States［C］//Proceedings of the 22nd Asian Test Symposium.New York，USA：ACM Press，2013：239-244.

［9］ Wang Jian.Functional Test Generation Guided by Steady-state Probabilities of Abstract Design［C］// Proceedings of Conference on Design Automation and Test in Europe.Berlin，Germ any：Springer，2014：5-13.

［10］ 顧震宇.基于仿真的32位RISC微處理器的功能驗證方法［J］.小型微型計算機系統(tǒng)，2004，25（4）：752-756.

［11］ 段博海.銀河飛騰 DSP模擬驗證平臺的設(shè)計與實現(xiàn)［D］.長沙：國防科學(xué)技術(shù)大學(xué)，2006.

［12］ 羅漢青，梁利平，葉甜春.DSP隨機測試程序自動生成技術(shù)［J］.微電子學(xué)與計算機，2013，30（11）：154-159.

編輯 顧逸斐

Constraint Random Instruction Generation Method for General Processor Based on Instruction Template

LIU Jing1，WANG Tiancheng2，WANG Jian2，3，LI Huawei2
（1.College of Information Engineering，Xiangtan University，Xiangtan 411105，China；2.State Key Laboratory of Computer Architecture，Institute of Computing Technology，Chinese Academy of Sciences，Beijing 100190，China；3.University of Chinese Academy of Sciences，Beijing 100049，China）

Due to the increasing system complexity of hardware design，functional verification becomes the bottleneck of the design flow.General processor is one of the most complex designs of integrated circuits，and it brings a huge challenge on its functional verification.This paper proposes a constraint random instruction generation method，for the simulation-based verification of an ARM v8 processor.This instruction generation method is based on the templates that are extracted from the instruction set，which guide the valid ARM v8 instructions’generation，and can support a variety of functional scenarios’verification by adjusting the constraints.Based on automatically comparison of the results produced by the validation environment，it achieves fully verification of the processor，and 58 design mistakes are found.The achievement has a good foundation，for the subsequent FPGA hardware emulation.The verification results show that the method can obtain the structural coverage of 90%.

functional verification；general processor；instruction template；instruction generation；constraint random instruction

劉 婧，王天成，王 健，等.基于指令模板的通用處理器約束隨機指令生成方法［J］.計算機工程，2015，41（10）：309-313.

英文引用格式：Liu Jing，Wang Tiancheng，Wang Jian，et al.Constraint Random Instruction Generation Method for General Processor Based on Instruction Template［J］.Computer Engineering，2015，41（10）：309-313.

1000-3428（2015）10-0309-05

A

TP031.6

國家自然科學(xué)基金資助項目（61176040）。

劉 婧（1989-），女，碩士研究生，主研方向：集成電路驗證；王天成，工程師、碩士；王 健，博上研究生；李華偉，研究員。

2014-09-03

2014-11-05E-mail：liujing@ict.ac.cn