存儲控制器是很多芯片的關(guān)鍵接口部件,存儲控制器正確穩(wěn)定的運行是整個芯片穩(wěn)定工作的前提保證。在驗證存儲控制器正確性時,如果采用單一的模擬驗證方法則會遇到激勵不能遍歷所有狀態(tài)空間的問題,這樣便無法證明設(shè)計輸出的接口信號是否完全符合DDR4等存儲器接口標(biāo)準(zhǔn)。不僅如此,為了提升訪存效率,設(shè)計人員需要對存儲控制器讀寫請求的調(diào)度方法進(jìn)行優(yōu)化,因此讀寫請求的仲裁方法有較高的復(fù)雜性,所以本文主要針對存儲控制器讀寫請求隊列仲裁邏輯的正確性和存儲控制器各個輸出命令間時序關(guān)系的正確性進(jìn)行驗證分析和研究。本文首先分析了存儲控制器驗證環(huán)節(jié)遇到的困難,介紹了目前國內(nèi)外驗證存儲控制器的常用方法和幾種存儲控制器命令間時序關(guān)系正確性驗證中斷言的自動生成方法。然后介紹了三種常用的形式驗證方法,說明了模型檢測原理和環(huán)境創(chuàng)建方法、并簡要說明驗證中采用的基于斷言的驗證方法。通過介紹存儲控制器工作原理、結(jié)構(gòu)組成、輸出命令間時序關(guān)系、請求仲裁策略說明了存儲控制器的結(jié)構(gòu)和功能。形式驗證方法是運用數(shù)學(xué)原理來驗證設(shè)計的正確性,可以自動遍歷所有需要驗證的狀態(tài)空間,相比模擬驗證表現(xiàn)出了更好的完備性和高效性,所以本文提出了一種基于模型檢測的形... 

【文章來源】：安徽大學(xué)安徽省 211工程院校

【文章頁數(shù)】：76 頁

【學(xué)位級別】：碩士

【部分圖文】：

基于TDML的SVA斷言生成方法

安徽大學(xué)碩士學(xué)位論文9錯誤，工具發(fā)現(xiàn)錯誤時可以提供錯誤場景幫助驗證人員分析錯誤。根據(jù)形式驗證結(jié)果分析覆蓋率狀況，并通過分析后的結(jié)果優(yōu)化形式驗證環(huán)境，提高形式驗證覆蓋率。圖2.1模型檢測驗證方法示意圖下圖2.2是模型檢測查錯示意圖，在模型檢測時首先是根據(jù)設(shè)計需求定義輸入可以搜索的狀態(tài)范圍，在狀態(tài)搜索過程中工具會首先建立一個初始狀態(tài)，并進(jìn)行擴展進(jìn)入下一個狀態(tài)，除非有明確的狀態(tài)約束，否則擴展將一直進(jìn)行。在查找過程中可能會出現(xiàn)狀態(tài)重復(fù)的情況，但是不管過程如何，工具都會遍歷所有的狀態(tài)空間，然后工具會將所有狀態(tài)的輸出值和模型檢測中的標(biāo)準(zhǔn)值進(jìn)行對比檢查，在進(jìn)行斷言檢查的過程中，如果出現(xiàn)了輸出值不符合斷言屬性的狀況，模型檢測工具會反方向運行，推導(dǎo)出出錯時的輸入狀態(tài)，這就是上文中提到的工具給出反例的原理。圖2.2模型檢測查錯示意圖

安徽大學(xué)碩士學(xué)位論文9錯誤，工具發(fā)現(xiàn)錯誤時可以提供錯誤場景幫助驗證人員分析錯誤。根據(jù)形式驗證結(jié)果分析覆蓋率狀況，并通過分析后的結(jié)果優(yōu)化形式驗證環(huán)境，提高形式驗證覆蓋率。圖2.1模型檢測驗證方法示意圖下圖2.2是模型檢測查錯示意圖，在模型檢測時首先是根據(jù)設(shè)計需求定義輸入可以搜索的狀態(tài)范圍，在狀態(tài)搜索過程中工具會首先建立一個初始狀態(tài)，并進(jìn)行擴展進(jìn)入下一個狀態(tài)，除非有明確的狀態(tài)約束，否則擴展將一直進(jìn)行。在查找過程中可能會出現(xiàn)狀態(tài)重復(fù)的情況，但是不管過程如何，工具都會遍歷所有的狀態(tài)空間，然后工具會將所有狀態(tài)的輸出值和模型檢測中的標(biāo)準(zhǔn)值進(jìn)行對比檢查，在進(jìn)行斷言檢查的過程中，如果出現(xiàn)了輸出值不符合斷言屬性的狀況，模型檢測工具會反方向運行，推導(dǎo)出出錯時的輸入狀態(tài)，這就是上文中提到的工具給出反例的原理。圖2.2模型檢測查錯示意圖

【參考文獻(xiàn)】：
期刊論文
[1]一種基于腳本語言的DDR控制器的驗證方法[J]. 羅軍,郭濤,張修欽,王玉冰.  集成電路應(yīng)用. 2018(06)
[2]基于屬性的形式驗證技術(shù)及應(yīng)用[J]. 游余新.  中國集成電路. 2013(12)

博士論文
[1]基于UML2.0模型的測試與驗證方法[D]. 張琛.西安電子科技大學(xué) 2012
[2]列車運行控制系統(tǒng)分層形式化建模與驗證分析[D]. 呂繼東.北京交通大學(xué) 2011
[3]基于功能信息的驗證工程學(xué)及若干驗證技術(shù)研究[D]. 張多利.合肥工業(yè)大學(xué) 2005

碩士論文
[1]面向MC-SoC的驗證方法研究與實現(xiàn)[D]. 郭少成.電子科技大學(xué) 2019
[2]基于Coq的工控程序驗證[D]. 周敏.東南大學(xué) 2018
[3]基于SystemC的多通道DDR控制器建模設(shè)計[D]. 沈鵬程.南京大學(xué) 2018
[4]基于模型檢測的外設(shè)控制器驗證方法研究及應(yīng)用[D]. 王思琦.湖南大學(xué) 2018
[5]基于LCoS時序彩色顯示的DDR2 SDRAM控制器的設(shè)計與驗證[D]. 王長森.湘潭大學(xué) 2018
[6]高頻動態(tài)編碼信號采集與存儲系統(tǒng)研究[D]. 方國昌.中北大學(xué) 2018
[7]MC-SOC中存儲控制器的設(shè)計與驗證[D]. 陳捷.電子科技大學(xué) 2018
[8]從Murphi到Ocaml語言的編譯器及其在模型檢測中的應(yīng)用[D]. 范帥.北京交通大學(xué) 2017
[9]向量定點運算單元的形式化驗證[D]. 朱青.西安電子科技大學(xué) 2017
[10]一種基于DDR4控制器的訪存調(diào)度優(yōu)化策略[D]. 劇諾璇.西安電子科技大學(xué) 2017



本文編號：3300903