王 俊,劉 磊,張 龍,李思昆
(國防科學(xué)技術(shù)大學(xué)高性能計(jì)算國家重點(diǎn)實(shí)驗(yàn)室,湖南長沙410073)
根據(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ù)。
隨著電子系統(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)證原理圖
由于進(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)證流程
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)證方法。
基于選擇或繼承已有的先進(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ù)。
在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)一管理。
根據(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)證基本流程
使用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)證。
本文提出了多核事務(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.