王 俊，劉 磊，張 龍，李思昆

（國防科學(xué)技術(shù)大學(xué)高性能計(jì)算國家重點(diǎn)實(shí)驗(yàn)室，湖南長沙410073）

1 引言

根據(jù)2011年國際半導(dǎo)體技術(shù)發(fā)展路線圖（ITRS）預(yù)測［1］，未來10年集成電路仍將按照摩爾定律持續(xù)高速發(fā)展，2015年將采用15 nm工藝，2020年將采用10 nm工藝，2022年將實(shí)現(xiàn)8 nm工藝，片上處理器核數(shù)目也呈現(xiàn)出同摩爾定律相似的指數(shù)增長規(guī)律，設(shè)計(jì)復(fù)雜程度達(dá)到前所未有的高度，對處理器驗(yàn)證提出了嚴(yán)峻的挑戰(zhàn)。

目前工程應(yīng)用中，多核處理器體系結(jié)構(gòu)的設(shè)計(jì)和驗(yàn)證仍然主要集中在寄存器傳輸級和門級。常用的驗(yàn)證方法仍然是模擬驗(yàn)證。形式驗(yàn)證成為研究熱點(diǎn)，硅后驗(yàn)證研究也得到了更多的關(guān)注。眾多的研究顯示，在多核處理器項(xiàng)目中，驗(yàn)證耗費(fèi)的時(shí)間和資源最多，驗(yàn)證已成為片上多核處理器發(fā)展的重大障礙。

Mentor Graphics公司CEO WallyRhines認(rèn)為，目前驗(yàn)證能力需要提高100倍才能滿足當(dāng)前硬件發(fā)展需要［2］，而形式驗(yàn)證和高層次的事務(wù)級驗(yàn)證將可能帶來這100倍的提速。但是，目前支持事務(wù)級高層次驗(yàn)證理論與方法的研究仍處于發(fā)展階段，相應(yīng)的驗(yàn)證工具還比較匱乏。

模擬驗(yàn)證由于具有非完備性，即只能證明有錯(cuò)而不能證明無錯(cuò)，一般適用于在驗(yàn)證初期發(fā)現(xiàn)大量和明顯的設(shè)計(jì)錯(cuò)誤?；诟采w率驅(qū)動(dòng)的模擬矢量自動(dòng)生成是當(dāng)前多核處理器模擬驗(yàn)證技術(shù)的研究熱點(diǎn)［3～6］。由于當(dāng)今片上多核處理器設(shè)計(jì)的復(fù)雜性和龐大的規(guī)模，沒有一種方法或工具能生成完備的模擬向量。

形式驗(yàn)證對系統(tǒng)具有的性質(zhì)和最終實(shí)現(xiàn)的正確性進(jìn)行嚴(yán)格的證明，從數(shù)學(xué)上完備地證明系統(tǒng)是否實(shí)現(xiàn)了設(shè)計(jì)者的意圖，較好地彌補(bǔ)了模擬驗(yàn)證的完備性缺陷，已在多個(gè)領(lǐng)域得到廣泛應(yīng)用。形式驗(yàn)證主要分為靜態(tài)形式驗(yàn)證和半形式驗(yàn)證。靜態(tài)形式驗(yàn)證不需要添加激勵(lì)，也不需要仿真，常用的是等價(jià)性檢查（Equivalence Checking）。半形式驗(yàn)證混合了仿真技術(shù)和形式驗(yàn)證技術(shù)，常用的是等價(jià)性驗(yàn)證和模型檢驗(yàn)。至今形式驗(yàn)證存在狀態(tài)空間爆炸問題，驗(yàn)證規(guī)模仍較小。Stanford大學(xué)和CMU大學(xué)在模型檢驗(yàn)方面進(jìn)行了大量卓有成效的研究，Clarke E M提出完全自動(dòng)化的、反例指導(dǎo)的抽象精化方法——CEGAR（Counter－Example Guide Abstraction Refinement），成為自動(dòng)分析與驗(yàn)證大規(guī)模軟硬件系統(tǒng)的一種主要方法［7］。荷蘭Rad－boud大學(xué)Schmaltz J等［8］在NOC協(xié)議交互式推斷驗(yàn)證方面做了大量有效工作。

事務(wù)級應(yīng)用驗(yàn)證是在多核處理器系統(tǒng)事務(wù)級模型上，編譯運(yùn)行典型應(yīng)用程序，驗(yàn)證多核處理器系統(tǒng)的功能設(shè)計(jì)是否正確。既可縮短應(yīng)用軟件開發(fā)時(shí)間，又可更完備地驗(yàn)證多核處理器事務(wù)級模型的設(shè)計(jì)正確性。已有的多核處理器應(yīng)用驗(yàn)證大多都是基于硬件仿真器實(shí)現(xiàn)，運(yùn)行效率較高，驗(yàn)證周期長，代價(jià)昂貴。對事務(wù)級應(yīng)用驗(yàn)證重視不夠，應(yīng)用較少。

前述的多核處理器驗(yàn)證方法屬于單視圖驗(yàn)證，在實(shí)際驗(yàn)證應(yīng)用中存在局限性。要將已有的單視圖驗(yàn)證聯(lián)合使用，存在數(shù)據(jù)共享和數(shù)據(jù)交換困難、使用不方便等問題。將形式驗(yàn)證和模擬驗(yàn)證結(jié)合是目前的研究熱點(diǎn)。

本文提出多核處理器的事務(wù)級多視圖協(xié)同驗(yàn)證方法，是通過把已有不同類型的先進(jìn)驗(yàn)證工具集成應(yīng)用，充分發(fā)揮不同類型驗(yàn)證方法綜合應(yīng)用的優(yōu)勢，協(xié)同高效完成驗(yàn)證任務(wù)。

2 多核事務(wù)級模型多視圖協(xié)同驗(yàn)證方法

2.1 多核事務(wù)級模型多視圖協(xié)同驗(yàn)證原理

隨著電子系統(tǒng)級設(shè)計(jì)方法的發(fā)展，事務(wù)級建模與驗(yàn)證技術(shù)受到高度重視。事務(wù)級模型遵循計(jì)算、存儲(chǔ)、通信分離的理念進(jìn)行高層抽象建模，只關(guān)注周期精確的系統(tǒng)功能，隱藏了不必要的計(jì)算和通信細(xì)節(jié)。因此，模型的可讀性好，模擬效率高，既便于進(jìn)行系統(tǒng)架構(gòu)分析和方案探索，又可為早期軟件開發(fā)提供模擬平臺(tái)，也可以為RTL設(shè)計(jì)提供參考模型和驗(yàn)證平臺(tái)。

多核處理器事務(wù)級模型多視圖協(xié)同驗(yàn)證方法，是把模擬驗(yàn)證、形式驗(yàn)證、應(yīng)用驗(yàn)證三類驗(yàn)證方法看做三種驗(yàn)證視圖，采用統(tǒng)一集成平臺(tái)，構(gòu)建一體化驗(yàn)證環(huán)境。從而可在一體化驗(yàn)證環(huán)境中，充分發(fā)揮多種驗(yàn)證方法綜合應(yīng)用的優(yōu)勢，協(xié)同高效完成多核處理器的驗(yàn)證任務(wù)。其原理示意圖如圖1所示。

該方法針對多核事務(wù)級模型，通過構(gòu)建統(tǒng)一操作界面，把三個(gè)驗(yàn)證視圖所需工具集成到一個(gè)框架下，使得驗(yàn)證操作便捷高效；進(jìn)行全局?jǐn)?shù)據(jù)管理和一致性維護(hù)，有效控制三個(gè)視圖驗(yàn)證流程，不同驗(yàn)證視圖可同時(shí)運(yùn)行，多個(gè)驗(yàn)證人員也可并行協(xié)同工作；通過構(gòu)建模型庫、驗(yàn)證庫、應(yīng)用程序庫，實(shí)現(xiàn)多核部件模塊、驗(yàn)證模塊、應(yīng)用程序的重用，增強(qiáng)了平臺(tái)的可擴(kuò)展性和適用性。

Figure 1 Multi－view co－verification schematic of transaction－level models圖1 事務(wù)級模型多視圖協(xié)同驗(yàn)證原理圖

2.2 多核事務(wù)級模型多視圖協(xié)同驗(yàn)證流程

由于進(jìn)行模擬驗(yàn)證和形式驗(yàn)證的工具和方法多樣，每種應(yīng)用都有特定的配置和需求，構(gòu)建統(tǒng)一界面的集成環(huán)境需要充分考慮這些工具軟件的特性，理順操作流程和相互關(guān)系。同時(shí)，多視圖協(xié)同驗(yàn)證中的大量數(shù)據(jù)需要按照協(xié)同驗(yàn)證流程合理順暢地在各視圖之間傳遞。其基本驗(yàn)證流程如圖2所示。

為實(shí)現(xiàn)時(shí)鐘精確的模擬，需要首先使用SystemC建立周期精確的多核事務(wù)級模型；然后根據(jù)多核模型各模塊的特點(diǎn)，結(jié)合模擬驗(yàn)證和形式驗(yàn)證的各自優(yōu)勢，并行進(jìn)行。

基于設(shè)計(jì)IP重用和驗(yàn)證IP重用思想，模擬驗(yàn)證視圖采用具有模擬矢量自動(dòng)生成、覆蓋率驅(qū)動(dòng)、基于事務(wù)驗(yàn)證的UVM驗(yàn)證技術(shù)，或者基于SCV（SystemC Verification Library）庫，進(jìn)行模擬驗(yàn)證。形式驗(yàn)證視圖目前主要基于較成熟的模型檢測和等價(jià)性驗(yàn)證工具，可以對在模擬試圖中所設(shè)計(jì)并經(jīng)過模擬驗(yàn)證的模塊做進(jìn)一步驗(yàn)證，也可以對所建立的多核事務(wù)級模型的其他適合進(jìn)行形式驗(yàn)證的模塊進(jìn)行同步驗(yàn)證。

基于驗(yàn)證程序重用思想，從基準(zhǔn)測試程序庫選取基準(zhǔn)程序，或自定義應(yīng)用測試程序，交叉編譯為目標(biāo)平臺(tái)上的二進(jìn)制文件，在硬件模擬器上加載運(yùn)行，結(jié)果與標(biāo)準(zhǔn)輸出對比，進(jìn)行應(yīng)用驗(yàn)證。該視圖下也可以實(shí)現(xiàn)軟硬件協(xié)同驗(yàn)證，即在通過驗(yàn)證的正確多核模型上，開發(fā)調(diào)試適合該多核架構(gòu)的應(yīng)用程序。

Figure 2 Multi－view co－verification process of multicore transaction－level models圖2 多核事務(wù)級模型多視圖協(xié)同驗(yàn)證流程

3 基于SoCLib的多核事務(wù)級多視圖協(xié)同驗(yàn)證環(huán)境實(shí)現(xiàn)

3.1 SoCLib仿真平臺(tái)

SoCLib仿真平臺(tái)由法國TIMA Lab、Lip6等研究機(jī)構(gòu)與STMicrelectronics等知名企業(yè)聯(lián)合開發(fā)，是基于片上多核系統(tǒng)設(shè)計(jì)的、開源的ESL建模仿真開放平臺(tái)。該平臺(tái)的核心是使用SystemC建模的模型庫，包括ARM、MIPS、Nios等微處理器、總線及片上網(wǎng)絡(luò)、Cache、主存、各種外設(shè)等，均可以在標(biāo)準(zhǔn)SystemC環(huán)境中模擬仿真。使用SystemC建模能夠?qū)崿F(xiàn)功能模塊、通信模塊、軟件模塊和硬件模塊在各種系統(tǒng)級層次上的抽象，可以快速有效地建立軟件算法的精確模型，并對設(shè)計(jì)進(jìn)行仿真驗(yàn)證和優(yōu)化。其仿真速度可達(dá)到使用VHDL或Verilog建模的10～100倍，可有效減少設(shè)計(jì)驗(yàn)證周期，縮短產(chǎn)品開發(fā)時(shí)間。

SoCLib每種模型有兩種類型可供使用：CABA（Cycle Accurate/Bit Accurate）、TLM－DT（Transaction Level Modeling with Distributed Time），均采用VISA組織的IP標(biāo)準(zhǔn)化接口VCI進(jìn)行封裝，可實(shí)現(xiàn)時(shí)鐘周期精確的仿真。SoCLib平臺(tái)還支持運(yùn)行DNA/OS、Mutek H、NetBSD等多個(gè)嵌入式操作系統(tǒng)，也提供了多個(gè)用于系統(tǒng)調(diào)試、監(jiān)控、設(shè)計(jì)空間探測的工具。SoCLib核心庫、多核系統(tǒng)架構(gòu)、操作系統(tǒng)與應(yīng)用程序之間的關(guān)系如圖3所示。

SoCLib平臺(tái)由一組庫文件構(gòu)成，其所有部件都符合VCI/OCP通訊協(xié)議標(biāo)準(zhǔn)，可以方便地根據(jù)特定的應(yīng)用需求添加新的功能，是比較理想的多核事務(wù)級建模仿真平臺(tái)。

Figure 3 Relations among SoCLib libraries，multi－core platforms，operating systems and applications圖3 SoCLib庫、多核平臺(tái)、操作系統(tǒng)和應(yīng)用程序關(guān)系

基于SoCLib開發(fā)多核處理器事務(wù)級多視圖驗(yàn)證環(huán)境，主要優(yōu)點(diǎn)在于：（1）SoCLib所有部件都采用SystemC建模，模型封裝都符合VCI/OCP通訊協(xié)議標(biāo)準(zhǔn)，既可有效利用其模型資源，又易于添加新的部件功能；（2）SoCLib的多核系統(tǒng)架構(gòu)遵循計(jì)算、通信、存儲(chǔ)分離的理念進(jìn)行設(shè)計(jì)，互聯(lián)通信模型既可采用總線模型，也可采用片上網(wǎng)絡(luò)模型，易于重用已有的IP核，提高了構(gòu)建各種多核處理器體系結(jié)構(gòu)的效率；（3）Soclib對多核體系結(jié)構(gòu)的應(yīng)用程序編譯映射提供了較好的技術(shù)支持。因此，本文重點(diǎn)研究基于SoCLib的多核處理器事務(wù)級多視圖協(xié)同驗(yàn)證方法。

3.2 多核事務(wù)級模型多視圖協(xié)同驗(yàn)證環(huán)境MVIE架構(gòu)

基于選擇或繼承已有的先進(jìn)模擬平臺(tái)和程序編譯平臺(tái)的考慮，構(gòu)建多視圖協(xié)同驗(yàn)證環(huán)境MVIE（Multi－view Verification Integrated Environment）。MVIE是基于SoCLib仿真平臺(tái)構(gòu)建的，直接支持SystemC事務(wù)級建模和ESL硬件仿真，主要解決模擬驗(yàn)證、形式驗(yàn)證和應(yīng)用驗(yàn)證多視圖協(xié)同控制，驗(yàn)證數(shù)據(jù)管理傳遞的問題，支持多種驗(yàn)證方法，支持驗(yàn)證代碼重用。

該多視圖協(xié)同驗(yàn)證環(huán)境框架基本結(jié)構(gòu)如圖4所示，主要分為三個(gè)層次。一是環(huán)境基礎(chǔ)部分，包括基礎(chǔ)類庫和SoCLib事務(wù)級仿真平臺(tái)、共享模型庫及工程模型庫?；A(chǔ)類庫含SystemC類庫、SCV類庫、Python庫、C＋＋標(biāo)準(zhǔn)庫，用以支持整個(gè)平臺(tái)運(yùn)行。二是人機(jī)交互部分，主要包括人機(jī)界面及對應(yīng)三類視圖的工具集成。其中公共人機(jī)界面提供統(tǒng)一的操作接口，并根據(jù)不同驗(yàn)證視圖所需工具的集成需要，實(shí)現(xiàn)三類驗(yàn)證視圖界面。模擬驗(yàn)證視圖下集成代碼編輯器、應(yīng)用編譯器和波形查看器；形式驗(yàn)證視圖下集成Cache一致性驗(yàn)證工具、等價(jià)性驗(yàn)證工具、NoC驗(yàn)證工具；應(yīng)用驗(yàn)證視圖下集成硬件編譯器、交叉編譯器、可視化調(diào)試器。三是工程數(shù)據(jù)管理部分，實(shí)現(xiàn)三類視圖數(shù)據(jù)的收集、查詢、分析和一致性管理。由于數(shù)據(jù)信息量不大，為便于在多視圖間傳遞，采用XML描述和存儲(chǔ)數(shù)據(jù)。

3.3 多核事務(wù)級模型多視圖協(xié)同驗(yàn)證環(huán)境MVIE軟件實(shí)現(xiàn)

在Linux下安裝設(shè)置好SoCLib仿真環(huán)境，按照圖4所示環(huán)境架構(gòu)，使用Qt設(shè)計(jì)開發(fā)具有良好交互界面的集成軟件平臺(tái)MVIE，著重解決三個(gè)視圖協(xié)同驗(yàn)證的數(shù)據(jù)傳遞和管理問題、多個(gè)工具軟件的集成問題、多視圖協(xié)同驗(yàn)證集中展現(xiàn)方法，實(shí)現(xiàn)軟件環(huán)境的可用性、高效性和實(shí)用性。

Figure 4 Multi－view co－verification environment architecture of multi－core transaction－level models圖4 多核事務(wù)級模型多視圖協(xié)同驗(yàn)證環(huán)境系統(tǒng)架構(gòu)

MVIE軟件主界面如圖5所示，主要分為四個(gè)區(qū)域：

（1）位于頂部的功能菜單區(qū)，可選擇軟件所有功能，包括工程、建模、視圖、命令、幫助等。

（2）位于左側(cè)的功能切換區(qū)，包括快捷使用、快速建模、模擬驗(yàn)證、形式驗(yàn)證、應(yīng)用驗(yàn)證五類視圖，可根據(jù)使用者的選擇顯示不同的內(nèi)容。快捷使用視圖，用于快速入門和啟動(dòng)工程，顯示于軟件啟動(dòng)時(shí)，提供軟件使用的快速入門提示和快速啟動(dòng)工程的鏈接；快速建模視圖，用于基于已有模塊庫快速建立多核模型，若模型工程未建立則提示先建立工程，待模型工程建立后或工程已建立則顯示當(dāng)前工程文件，提供代碼編輯、編譯、調(diào)試功能；模擬驗(yàn)證視圖和形式驗(yàn)證視圖用于使用相關(guān)工具對特定模塊進(jìn)行驗(yàn)證，若模塊工程未建立則建立模塊工程，若模塊工程已建立則顯示模塊工程主文件內(nèi)容，提供代碼編輯、編譯、調(diào)試和基于工具的驗(yàn)證功能；應(yīng)用驗(yàn)證視圖用于使用自選的應(yīng)用程序驗(yàn)證多核模型，或者在已驗(yàn)證的多核模型上開發(fā)多核應(yīng)用軟件，提供代碼編輯、編譯、調(diào)試和程序運(yùn)行結(jié)果對比功能。

（3）文件列表區(qū)，分為工程文件列表和庫文件列表。其中，工程文件列表列出當(dāng)前工程所有文件，便于查看和組織工程源文件；庫文件列表列出公用IP模塊庫和自定義模塊庫所有模塊，方便查看和調(diào)用。工程文件列表根據(jù)視圖選擇的不同進(jìn)行相應(yīng)的變化，快速建模和應(yīng)用驗(yàn)證視圖下顯示模型工程文件列表，模擬驗(yàn)證和形式驗(yàn)證視圖下顯示模塊工程文件列表，并提供導(dǎo)入/導(dǎo)出、添加/刪除代碼文件的功能；庫文件列表根據(jù)視圖選擇的不同進(jìn)行相應(yīng)變化，快速建模視圖下顯示為SoCLib內(nèi)置IP庫和用戶自定義IP庫，模擬驗(yàn)證和形式驗(yàn)證視圖則顯示為工具列表，應(yīng)用驗(yàn)證視圖下顯示為應(yīng)用程序庫。

（4）顯示區(qū)，包括代碼顯示區(qū)和編譯信息顯示區(qū)。代碼顯示區(qū)主要提供代碼顯示、編輯功能；編譯信息顯示區(qū)顯示與當(dāng)前視圖相關(guān)的編譯輸出、驗(yàn)證結(jié)果等，還提供命令行功能，可使用soclib cc命令執(zhí)行某些編譯操作。

Figure 5 Main interface of software MVIE圖5 MVIE軟件主界面

MVIE主要信息分為兩類：工程文件和驗(yàn)證信息。工程文件分兩種：（1）模型，用于構(gòu)建完整的多核模型，在快速建模和應(yīng)用驗(yàn)證兩類視圖下使用；（2）模塊，用于自主編寫單個(gè)模塊并據(jù)此進(jìn)行驗(yàn)證，在模擬驗(yàn)證和形式驗(yàn)證兩類視圖下使用。工程文件的XML信息主要描述相關(guān)文件組織結(jié)構(gòu)、進(jìn)行版本記錄等。驗(yàn)證信息也分兩種，（1）模型驗(yàn)證信息，用于對整個(gè)多核模型的運(yùn)行和驗(yàn)證情況進(jìn)行記錄，在快速建模和應(yīng)用驗(yàn)證視圖下使用；（2）模塊驗(yàn)證信息，用于對特定的模塊的運(yùn)行和驗(yàn)證情況進(jìn)行記錄，在模擬驗(yàn)證和形式驗(yàn)證視圖下使用。模型驗(yàn)證信息記錄多核模型的主要結(jié)構(gòu)參數(shù)和應(yīng)用驗(yàn)證的結(jié)果數(shù)據(jù)，用于對多核模型的整體評估；模塊驗(yàn)證信息記錄當(dāng)前模塊主要信息和進(jìn)行模擬驗(yàn)證、形式驗(yàn)證的結(jié)果數(shù)據(jù)，并進(jìn)行模塊版本記錄，用于控制模塊驗(yàn)證過程。軟件采用XML描述相關(guān)信息，各視圖之間傳遞XML文件，軟件對所有XML文件統(tǒng)一管理。

4 多視圖協(xié)同驗(yàn)證環(huán)境MVIE的使用

4.1 多視圖協(xié)同驗(yàn)證環(huán)境MVIE的使用流程

根據(jù)多核事務(wù)級模型的建立方法的不同，多視圖協(xié)同驗(yàn)證環(huán)境MVIE的使用流程分為兩種類型：（1）可稱為集成建模，即基于現(xiàn)有模塊庫進(jìn)行快速建模后，直接進(jìn)行應(yīng)用驗(yàn)證，驗(yàn)證模型建模正確性，分析體系結(jié)構(gòu)性能，進(jìn)行多核應(yīng)用開發(fā)；（2）可稱為標(biāo)準(zhǔn)建模，即用戶使用SystemC自主開發(fā)部分組件模塊，使用模擬驗(yàn)證和形式驗(yàn)證驗(yàn)證其正確性后，按照VCI規(guī)范，結(jié)合IP庫中已有模塊，構(gòu)建多核模型，再進(jìn)行應(yīng)用驗(yàn)證，進(jìn)一步驗(yàn)證建模正確性，分析體系結(jié)構(gòu)性能，進(jìn)行多核應(yīng)用開發(fā)。使用MVIE進(jìn)行多視圖協(xié)同驗(yàn)證的基本流程如圖6所示，其中圖6a為集成建模下多視圖協(xié)同驗(yàn)證基本流程，圖6b為標(biāo)準(zhǔn)建模下多視圖協(xié)同驗(yàn)證基本流程。

Figure 6 Basic process of multi－view co－verification using MVIE圖6 使用MVIE進(jìn)行多視圖協(xié)同驗(yàn)證基本流程

4.2 多視圖協(xié)同驗(yàn)證環(huán)境MVIE使用實(shí)例

使用MVIE，可使用SystemC進(jìn)行硬件模塊建模，采用VCI規(guī)范封裝后集成到SoCLib平臺(tái)進(jìn)行模擬驗(yàn)證、形式驗(yàn)證、應(yīng)用驗(yàn)證；也可直接基于SoCLib平臺(tái)提供的SystemC模型庫進(jìn)行集成建模，分析驗(yàn)證所構(gòu)建的多核系統(tǒng)。由于多視圖協(xié)同驗(yàn)證環(huán)境MVIE的使用流程中，標(biāo)準(zhǔn)建模驗(yàn)證已包含了集成建模驗(yàn)證的過程，因此進(jìn)行標(biāo)準(zhǔn)建模驗(yàn)證實(shí)驗(yàn)即可完整檢驗(yàn)所建立的MVIE環(huán)境。

實(shí)驗(yàn)自主設(shè)計(jì)的用SystemC描述的1 KB RAM事務(wù)級模型，基于SCV進(jìn)行模擬驗(yàn)證。用SystemC描述多核Cache一致性協(xié)議的事務(wù)級模型，使用NuSMV模型檢驗(yàn)工具進(jìn)行形式驗(yàn)證。使用該RAM事務(wù)級模型和Cache一致性協(xié)議模型，基于SoCLib平臺(tái)構(gòu)建雙核系統(tǒng)，運(yùn)行MJPEG解碼程序進(jìn)行應(yīng)用驗(yàn)證。

在MVIE環(huán)境下，首先使用MVIE快速建模功能在模擬驗(yàn)證視圖下建立RAM的模塊工程，使用SystemC編寫事務(wù)級模型代碼?；赟CV構(gòu)建自檢測驗(yàn)證平臺(tái)［9］，編寫Stimulus模塊、BFM/FIFO模塊、Write Adaptor模塊、Read Adaptor模塊、Reference Model模塊、Checker模塊，使用SCV提供的測試向量生成機(jī)制進(jìn)行模擬驗(yàn)證，輸出結(jié)果與數(shù)學(xué)模型［10］結(jié)果比較。

在形式化驗(yàn)證視圖下，我們使用SystemC構(gòu)建多核Cache一致性協(xié)議事務(wù)級模塊，并通過基于謂詞的自動(dòng)化抽象和模型轉(zhuǎn)換技術(shù)生成Kripke結(jié)構(gòu)，最后調(diào)用NuSMV模型檢驗(yàn)工具對該模塊進(jìn)行形式驗(yàn)證［11］。在快速建模視圖下，建立多核模型工程。對上述建立的兩個(gè)模塊按照VCI規(guī)范封裝，再從SoCLib共享模型庫中選擇所需模塊，如MIPS處理器、片上網(wǎng)絡(luò)GMN（Generic Micronetwork）、顯示設(shè)備VCI＿TTY模塊、定時(shí)器VCI＿TIMER、文件系統(tǒng)VCI＿FDACCESS、幀緩存VCI＿FRAMEBUFFER、同步鎖VCI＿LOCKS，使用頂層描述文件描述雙核硬件平臺(tái)，并調(diào)用硬件編譯器編譯SystemCASS成可執(zhí)行硬件模擬平臺(tái)。使用C＋＋編寫MJPEG解碼程序，調(diào)用MIPS交叉編譯器編譯成二進(jìn)制文件，在可執(zhí)行硬件模擬平臺(tái)上運(yùn)行，進(jìn)行應(yīng)用驗(yàn)證。

5 結(jié)束語

本文提出了多核事務(wù)級模型多視圖協(xié)同驗(yàn)證方法，并論述了多視圖協(xié)同驗(yàn)證環(huán)境的架構(gòu)，最后實(shí)現(xiàn)了該環(huán)境MVIE。該方法針對高層次事務(wù)級建模需要，基于開放的SoCLib事務(wù)級仿真平臺(tái)，將模擬驗(yàn)證、形式驗(yàn)證和應(yīng)用驗(yàn)證有機(jī)結(jié)合起來。使用MVIE可基于SoCLib平臺(tái)快速構(gòu)建多核事務(wù)級模型，大大縮短復(fù)雜多核系統(tǒng)事務(wù)級模型開發(fā)時(shí)間，提高建模效率；多個(gè)驗(yàn)證視圖切換由軟件控制，各視圖間驗(yàn)證數(shù)據(jù)使用XML交互，能充分發(fā)揮三種不同驗(yàn)證手段的優(yōu)勢，提高驗(yàn)證效率；不同模塊可在不同的視圖下并行驗(yàn)證，有利于驗(yàn)證人員分工合作，加快驗(yàn)證工作進(jìn)程。但是，由于多核系統(tǒng)模型的復(fù)雜性，多視圖下的協(xié)同驗(yàn)證的數(shù)據(jù)收集還比較簡單，且目前形式驗(yàn)證技術(shù)發(fā)展尚不成熟，支持形式驗(yàn)證的工具方法非常有限，下一步將針對細(xì)化多視圖協(xié)同驗(yàn)證數(shù)據(jù)、豐富形式驗(yàn)證工具、提高多視圖驗(yàn)證協(xié)同度進(jìn)行更深入的研究。

［1］ Jiang Shan，Huang Jian，Wang Gui－fang，et al.A brief of the international technology roadmap for semiconductors（ITRS）：Executive summary，2011［J］.Dynamic Monitoring of Science Letters，2012（4）：1－2.（in Chinese）

［2］ Foster H.Ending endless verification with questa formal verification［C］∥Proc of DVCon’08，2008：1.

［3］ Shimizu K，Gupta S，Koyama T，et al.Verification of the cell broadband engineTMprocessor［C］∥Proc of the 43rd Design Automation Conference，2006：1.

［4］ Schubert K－D.POWER7—Verification challenge of a multicore processor［C］∥Proc of the 2009 International Conference on Computer－Aided Design（ICCAD09），2009：809－812.

［5］ Turumella B，Sharma M.Assertion－based verification of a 32 thread SPARCTMCMT microprocessor［C］∥Proc of the 45th Design Automation Conference，2008：256－261.

［6］ Chen Xiao－fang，Yang Yu，Gopalakrishnan G，et al.Reducing verification complexity of a multicore coherence protocol using assume/guarantee［C］∥Proc of FMCAD’06，2006：81－88.

［7］ Borrione D，Helmy A，Pierre L V，et al.A generic model for formally verifying NoC communication architectures：A case study［C］∥Proc of NOCS’07，2007：127－136.

［8］ Chen Xiao－fang，Yang Yu，Gopalakrishnan G，et al.Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols［J］.Formal Methods in System Design，2010，36（1）：37－64.

［9］ Fang Liang，Rong Meng－tian，Liu Wen－jiang，et al.Modeling of transaction－level verification based on systemC verification library［J］.Computer Engineering，2007，33（15）：238－240.（in Chinese）

［10］ Silva D，Araujo M.An automatic testbench generation tool for a systemC functional verification methodology［C］∥Proc of the 17th Symposium on Integrated Circuits and System Design，2004：66－70.

［11］ Zhang Long.Research and implementation of model checking cache coherence protocol for multi－core processor［D］.Changsha：National University of Defence Technology，2012.（in Chinese）

附中文參考文獻(xiàn)：

［1］ 姜山，黃健，王桂芳，等.2011版國際半導(dǎo)體技術(shù)路線圖部分更新內(nèi)容摘要［J］.科學(xué)研究動(dòng)態(tài)監(jiān)測快報(bào)，2012（4）：1－2.

［9］ 方亮，戎蒙恬，劉文江，等.基于SCV的事務(wù)級驗(yàn)證建模［J］.計(jì)算機(jī)工程，2007，33（15）：238－240.

［11］ 張龍.多核處理器Cache一致性協(xié)議模型檢驗(yàn)研究與實(shí)現(xiàn)［D］.長沙：國防科學(xué)技術(shù)大學(xué)，2012.