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

【引證文獻】

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

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

，

本文編號：2687842