多核處理器事務級模型多視圖協(xié)同驗證環(huán)境＊

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

（國防科學技術大學高性能計算國家重點實驗室，湖南長沙410073）

1 引言

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3.1 SoCLib仿真平臺

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

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

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

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

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

3.2 多核事務級模型多視圖協(xié)同驗證環(huán)境MVIE架構

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

5 結束語

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

［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）

附中文參考文獻：

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

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

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