本文關鍵詞：基于SOC異步FIFO的設計與形式驗證

  更多相關文章： SOC 異步FIFO 形式驗證 JASPER

【摘要】：近年,隨著集成電路產業(yè)的快速發(fā)展,半導體工藝水平已經達到亞微米水平,隨之而來的現(xiàn)狀就是芯片集成規(guī)模越來越復雜。縱觀整個芯片設計流程,從行為級HDL一直到芯片最后的投片,最復雜、最重要的環(huán)節(jié)就是驗證。在面對更大的驗證壓力時,傳統(tǒng)的模擬仿真驗證已經漸漸暴露出其局限性。形式驗證方法作為傳統(tǒng)驗證方法的補充,日益引起人們的關注。形式驗證方法以不同的驗證邏輯實現(xiàn)驗證目標,能夠克服傳統(tǒng)驗證方法的不足,所以本文的研究重心為形式驗證,并結合JASPER平臺提出了適用性更廣的形式驗證方法。首先,本文選取SOC中常用模塊異步FIFO為驗證對象,基于傳統(tǒng)異步FIFO設計結構和功能實現(xiàn)邏輯,本文提出了改進后的異步FIFO設計,與傳統(tǒng)設計相比,改進后的設計優(yōu)勢在于運用了新的空滿標志位判斷邏輯,克服了傳統(tǒng)設計中存儲器深度的局限性;然后,本文分析了形式驗證當前的應用局限性,研究了基于Jasper平臺形式驗證方法的邏輯原理以及形式驗證狀態(tài)空間的意義,并對Jasper平臺特征驗證流程進行了詳細的說明,同時,引入了Jasper的特征驗證語言SVA,通過舉例分析研究了SVA語言關于設計特性的描述細則;最后,以本文中改進后的異步FIFO為驗證對象,制定出特定的Jasper驗證方案,并基于異步FIFO設計的功能劃分進行斷言語句的編寫,在驗證結果分析中,通過特征語句編寫錯誤為例詳細討論了如何使用Jasper圖形界面進行驗證分析糾錯。本文形式驗證方法的研究結果表明,基于JASPER平臺的形式驗證方法較傳統(tǒng)模擬仿真方法,具有無需編寫Testbench與Testcase、驗證周期短、驗證覆蓋率高等特點。目前,本文所研究的形式驗特征驗證方法已經廣泛用于INTEL SOC驗證項目中,多為與模擬仿真方法相結合,大大提高了原始單一方法驗證的效率。形式驗證方法的研究對未來數(shù)字IC驗證的發(fā)展具有極其深遠的實際意義,同時,對日益復雜的數(shù)字IC設計也提供了充分的驗證保障。
【學位授予單位】：西安電子科技大學
【學位級別】：碩士
【學位授予年份】：2015
【分類號】：TP333

【共引文獻】

中國期刊全文數(shù)據庫 前10條

1 鄭慶偉;周武;余躍;;航天IP核的自主設計、評測關鍵技術研究[J];航天標準化;2012年02期

2 楊軍;葛海通;鄭飛君;嚴曉浪;;一種形式化驗證方法:模型檢驗[J];浙江大學學報(理學版);2006年04期

3 王海峰,呂永波,張仲義;一種系統(tǒng)安全性的形式化驗證方法[J];計算機工程與應用;2003年04期

4 李光輝,邵明,李曉維;通用CPU設計驗證中的等價性檢驗方法[J];計算機輔助設計與圖形學學報;2005年02期

5 魯巍;呂濤;楊修濤;李曉維;;RTL可觀測性語句覆蓋評估方法[J];計算機輔助設計與圖形學學報;2006年01期

6 李光輝,邵明,李曉維;驗證包含黑盒的電路設計的有效方法[J];計算機學報;2004年06期

7 張仲義,王海峰;智能交通安全控制系統(tǒng)的模型驗證[J];交通運輸工程與信息學報;2003年01期

8 胡東華;張旭;;模擬退火算法在BDD變量最優(yōu)排序中的應用[J];科技信息(科學教研);2007年34期

9 岳園;何安平;;使用邏輯錐分割的組合電路等價性驗證[J];計算機工程與應用;2013年02期

10 谷偉卿;施智平;關永;張杰;趙春娜;葉世偉;;Gauge積分在HOL4中的形式化[J];計算機科學;2013年02期

中國碩士學位論文全文數(shù)據庫 前10條

1 李鴻翔;基于VMM的硬件驗證技術研究及應用[D];哈爾濱工程大學;2010年

2 閆碩;基于多項式符號代數(shù)的電路形式驗證[D];北京交通大學;2011年

3 劉林;數(shù)字集成電路功能驗證中的變異測試方法研究[D];山東大學;2011年

4 馬麗麗;基于靜態(tài)分析的RTL設計錯誤檢測方法研究[D];湘潭大學;2011年

5 王瑞蛟;安全SoC體系結構的設計與實現(xiàn)研究[D];解放軍信息工程大學;2011年

6 吳俊華;組合電路的形式驗證方法研究[D];哈爾濱工程大學;2004年

7 李樹杰;中科SoC通用驗證平臺及驗證方法學研究[D];山東科技大學;2005年

8 胡靖;可再配置結構中針對IP重用技術的綜合方法研究[D];哈爾濱工程大學;2005年

9 鄭偉偉;基于線性規(guī)劃的RTL性質驗證研究[D];清華大學;2005年

10 王迪;微處理器的分級模型檢驗驗證研究[D];清華大學;2005年

，

本文編號：1176944