【摘要】：隨著芯片系統(tǒng)的功能日益復(fù)雜,上市時(shí)間卻越來越短,越來越多的芯片系統(tǒng)希望實(shí)現(xiàn)為片上系統(tǒng)(SoC)。SoC是指集成有包括微處理器、存儲(chǔ)器等各種硬件模塊,以及運(yùn)行于它們之上的嵌入式軟件,以完成特定目標(biāo)的系統(tǒng)。SoC的特點(diǎn)在于大量的系統(tǒng)功能以運(yùn)行于硬件平臺(tái)之上的嵌入式軟件實(shí)現(xiàn),因此開發(fā)更加靈活,周期更短。傳統(tǒng)的芯片系統(tǒng)設(shè)計(jì)流程從描述系統(tǒng)的寄存器傳輸級(jí)(RTL)模型開始,難以適應(yīng)嵌入式軟件早期開發(fā)的要求,因此不適合SoC開發(fā)。新提出的開發(fā)流程從描述系統(tǒng)的事務(wù)級(jí)模型(TLM)開始。事務(wù)級(jí)比RTL抽象層次高,因此TLM開發(fā)更加容易,仿真速度也更快,可作為嵌入式軟件早期開發(fā)的平臺(tái),適合SoC開發(fā)。SystemC是目前事務(wù)級(jí)建模的標(biāo)準(zhǔn)語(yǔ)言,因此針對(duì)SystemC模型開發(fā)和驗(yàn)證技術(shù)的研究具有重要意義。 本文首先提出將針對(duì)同一SoC項(xiàng)目開發(fā)的一組SystemC模型視為一種特殊的軟件產(chǎn)品線(SPL),稱為SystemC模型產(chǎn)品線(SCPL),然后研究了SCPL的開發(fā)方法、組合安全性和形式化功能驗(yàn)證問題。SPL指針對(duì)同一領(lǐng)域開發(fā)的一組軟件的集合。由于針對(duì)同一領(lǐng)域,這組軟件間存在很多公共特征,SPL相關(guān)研究旨在利用這些公共特征提高軟件的開發(fā)和驗(yàn)證效率。SCPL是針對(duì)同一SoC項(xiàng)目開發(fā)的一組SystemC模型,模型間同樣存在很多公共特征,如何利用它們提高SystemC模型的開發(fā)和驗(yàn)證效率,是本文的研究目標(biāo)�？紤]到SystemC模型本質(zhì)是C++程序,因此SCPL研究可借鑒SPL研究成果。考慮到SystemC模型旨在模擬硬件的并發(fā)行為,而軟件是順序執(zhí)行的,因此SCPL研究與SPL研究存在差異。SPL研究主要包括四項(xiàng)內(nèi)容,即開發(fā)方法、語(yǔ)法正確性、組合安全性和行為正確性。本文針對(duì)SCPL在以上四項(xiàng)內(nèi)容開展了相應(yīng)研究,取得了如下研究成果: (1)論證了以TLM為入口的芯片設(shè)計(jì)新流程下,SoC設(shè)計(jì)過程往往伴隨著一組SystemC模型的開發(fā),首次提出將這組SystemC模型視為一種特殊的SPL,并稱之為SystemC模型產(chǎn)品線(SCPL)。指出了SCPL與普通SPL的異同。 (2)指出了以傳統(tǒng)的面向?qū)ο蠓椒ㄩ_發(fā)SCPL存在的問題,提出以面向特征的方法開發(fā)SCPL。指出現(xiàn)有的面向特征方法在開發(fā)SCPL時(shí)存在的問題,提出了解決方案,并提出一套相應(yīng)的面向特征的SCPL開發(fā)方法。案例研究表明,與面向?qū)ο箝_發(fā)方法相比,面向特征的SCPL開發(fā)方法可有效減少重復(fù)代碼,提高開發(fā)效率。同時(shí),與基于條件編譯的SCPL開發(fā)方法相比,面向特征的SCPL開發(fā)方法可有效減少處于條件編譯指令包圍中的代碼。由于條件編譯指令的大量使用是造成代碼難以開發(fā)、理解和維護(hù)的關(guān)鍵,因此本文提出的面向特征的SCPL開發(fā)方法可以提高SCPL開發(fā)效率,增強(qiáng)代碼的可理解性和可維護(hù)性。 (3)提出了一套簡(jiǎn)化的SystemC語(yǔ)言SC~S及其面向特征的擴(kuò)展FSC~S,討論了以FSC~S開發(fā)的SCPL的組合安全性問題,給出了一套可靠且完全的形式化判定方法。要判定SCPL的組合安全性,傳統(tǒng)方法只能逐個(gè)編譯SCPL中所有的SystemC模型,與這種方法相比,本文的判定方法可以顯著縮短判定時(shí)間,提高判定效率。 (4)基于屬性保持的概念提出一種SCPL形式化功能驗(yàn)證方法,案例研究表明,與枚舉SCPL中所有SystemC模型并逐個(gè)驗(yàn)證的方法相比,該方法能有效減少待驗(yàn)證SystemC模型的數(shù)目,從而有效改善SCPL形式化功能驗(yàn)證所需的時(shí)間和空間消耗。 (5)提出了屬性推斷的概念,并基于此概念提出一種SCPL形式化功能驗(yàn)證方法。與屬性保持相比,屬性推斷的要求更加寬松,因此相應(yīng)的SCPL形式化功能驗(yàn)證方法適用范圍更廣。案例研究表明,與枚舉SCPL中所有SystemC模型并逐個(gè)驗(yàn)證的方法相比,基于屬性推斷的方法能顯著減少待驗(yàn)證SystemC程序的數(shù)目,從而顯著改善驗(yàn)證所需的時(shí)間和空間消耗。 本文以面向特征的SCPL開發(fā)方法完成了OpenRisc 1000項(xiàng)目和MJPEG解碼芯片項(xiàng)目的開發(fā)。并針對(duì)前一項(xiàng)目使用本文提出的方法進(jìn)行了組合安全性判定和形式化功能驗(yàn)證。前一項(xiàng)目的開發(fā)與OpenCores組織提供的開源實(shí)現(xiàn)相比,處于條件編譯指令包圍中的代碼量顯著減少,從而改善了代碼的可理解性和可維護(hù)性。后一項(xiàng)目的實(shí)現(xiàn)與面向?qū)ο蟮腟CPL實(shí)現(xiàn)相比,代碼總量大幅減少,從而提高了開發(fā)效率。針對(duì)OpenRisc 1000項(xiàng)目的組合安全性判定結(jié)果顯示,本文提出的方法比基于枚舉的判定方法驗(yàn)證效率大幅提高。針對(duì)OpenRisc 1000項(xiàng)目的形式化功能驗(yàn)證結(jié)果表明,與基于枚舉的判定方法相比,本文提出的基于屬性保持的方法能夠有效減少判定所需的時(shí)間和空間消耗,本文提出的基于屬性推斷的方法能顯著減少判定所需的時(shí)間和空間消耗。
【學(xué)位授予單位】：國(guó)防科學(xué)技術(shù)大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2011
【分類號(hào)】：TP368.1;TN47

【引證文獻(xiàn)】

相關(guān)碩士學(xué)位論文 前1條

1 曾宇森;視線跟蹤SoC的系統(tǒng)建模及驗(yàn)證[D];華南理工大學(xué);2012年

，

本文編號(hào)：2687842