縱觀整個芯片設計流程,從最初的架構設計到最后的投片,驗證是用時最長且重要性最高的環(huán)節(jié)。對目前納米級的設計規(guī)模而言,傳統(tǒng)的動態(tài)驗證方式已經(jīng)不足以完成對整體設計的驗證工作。形式驗證方法因為驗證覆蓋的完備性,面對大規(guī)模設計的高效性,非常切合芯片后端物理實現(xiàn)的驗證需求,因而越發(fā)廣泛地被業(yè)界采用。如何對驗證失敗的情況進行分析,快速準確地定位問題,并提供可行的調(diào)試方案,已成為實際工程領域關注的重點。本論文在較為全面地研究總結當前廣泛應用于芯片后端設計實現(xiàn)的形式驗證技術的基礎上,結合自身在實習期間的項目經(jīng)歷,對形式驗證在數(shù)字LTE芯片實際工程中所采用的邏輯等價性對比進行了分析,取得了較為理想的結果。主要內(nèi)容包括:首先在數(shù)字LTE芯片形式驗證的流程方面,論文將芯片形式驗證的流程細化為環(huán)境搭建、初始化、讀入文件和約束、選項設置和等價性對比五個步驟,使后續(xù)工作中對結果進行分析和調(diào)試的范圍更加清晰。結合LEC工具的指令對具體的運行腳本進行規(guī)范,明確了驗證過程中必要的指令及相關選項。并且基于平展化和層次化這兩種不同的邏輯等價性對比方式,分別對其各自的原理、實現(xiàn)方法和特點進行分析。然后在邏輯等價性對比結果方面,... 

【文章來源】：西安電子科技大學陜西省 211工程院校 教育部直屬院校

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

【學位級別】：碩士

【文章目錄】：
摘要
ABSTRACT
縮略語對照表
第一章 緒論
    1.1 論文背景及意義
    1.2 國內(nèi)外研究現(xiàn)狀
    1.3 論文研究重點及章節(jié)安排
第二章 驗證方法學綜述
    2.1 動態(tài)驗證技術
    2.2 靜態(tài)驗證技術
        2.2.1 靜態(tài)時序驗證
        2.2.2 設計規(guī)則驗證
        2.2.3 版圖驗證
    2.3 形式驗證方法
        2.3.1 定理證明
        2.3.2 模型檢測
        2.3.3 等價性驗證
    2.4 工程中的形式驗證
        2.4.1 形式驗證工具簡介
        2.4.2 LEC的等價性驗證方法
    2.5 本章小結
第三章 LEC形式驗證的流程
    3.1 LEC形式驗證準備階段
        3.1.1 環(huán)境搭建
        3.1.2 初始化
        3.1.3 讀入文件和約束
        3.1.4 選項設置
    3.2 LEC形式驗證對比階段
        3.2.1 平展化模式
        3.2.2 層次化模式
    3.3 本章小結
第四章 邏輯等價性驗證的結果分析
    4.1 平展化模式的調(diào)試思路
    4.2 平展化模式的結果分析
        4.2.1 文件缺失
        4.2.2 名稱錯誤
        4.2.3 UPF問題
        4.2.4 掃描信號參與邏輯
        4.2.5 設計或綜合問題
    4.3 層次化模式的調(diào)試思路
    4.4 層次化模式的結果分析
        4.4.1 DesignWare問題
        4.4.2 實例化問題
    4.5 等價性驗證中斷問題
        4.5.1 中斷的成因及危害
        4.5.2 避免中斷的方法
        4.5.3 傳統(tǒng)的中斷解決方法
        4.5.4 采用隔離對比法解決中斷
    4.6 本章小結
第五章 總結與展望
    5.1 論文工作總結
    5.2 進一步的工作展望
參考文獻
致謝
作者簡介


【參考文獻】：
期刊論文
[1]基于邏輯的形式化驗證方法:進展及應用[J]. 陳鋼,于林宇,裘宗燕,王穎.  北京大學學報(自然科學版). 2016(02)
[2]片上系統(tǒng)高層等價性檢驗研究進展[J]. 胡健,李暾,李思昆.  計算機輔助設計與圖形學學報. 2016(03)
[3]集成電路技術和產(chǎn)業(yè)發(fā)展現(xiàn)狀與趨勢[J]. 方圓,徐小田.  微電子學. 2014(01)
[4]SpaceWire譯碼電路在HOL4中的形式化驗證[J]. 張玉鵬,施智平,關永,李黎明,趙春娜,張杰.  小型微型計算機系統(tǒng). 2013(08)
[5]模型檢測中狀態(tài)爆炸問題研究綜述[J]. 侯剛,周寬久,勇嘉偉,任龍濤,王小龍.  計算機科學. 2013(S1)
[6]基于IP技術的模擬集成電路設計研究[J]. 李群,樊麗春.  科技創(chuàng)新導報. 2013(08)
[7]數(shù)字電路IP軟核任務流方法驗證[J]. 何朝軍,李哲英.  電子測量技術. 2011(08)
[8]集成電路技術的發(fā)展[J]. 陳飚.  微處理機. 2011(03)
[9]利用SMT約束分解方法求解RTL可滿足性問題[J]. 趙燕妮,邊計年,鄧澍軍.  計算機輔助設計與圖形學學報. 2010(02)
[10]基于混合自動機的PSL模型研究[J]. 張萌,高德遠,樊曉椏.  計算機應用研究. 2010(01)

博士論文
[1]模型檢測中關鍵技術的研究及其應用[D]. 劉志鋒.南京大學 2011
[2]集成電路的邏輯等價性驗證研究[D]. 楊軍.浙江大學 2007
[3]超大規(guī)模集成電路形式驗證的方法研究[D]. 盧永江.浙江大學 2005

碩士論文
[1]基于圖論的形式化驗證方法的研究與實現(xiàn)[D]. 陳凌宇.電子科技大學 2016
[2]基于SOC Encounter的ASIC芯片后端設計研究[D]. 駱禮廳.西安電子科技大學 2014
[3]基于UVM的高效驗證平臺設計及可重用性研究[D]. 黃欣.上海交通大學 2014
[4]基于多項式符號代數(shù)的電路形式驗證[D]. 閆碩.北京交通大學 2011
[5]異步FIFO的設計與形式化驗證[D]. 劉彬.國防科學技術大學 2011
[6]大規(guī)模數(shù)字集成電路中的驗證技術及其應用[D]. 廉玉平.浙江大學 2010
[7]0.35um標準單元庫的設計技術研究及實現(xiàn)[D]. 黃義定.江南大學 2006



本文編號：3187129