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

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

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

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

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


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

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

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



本文編號：3187129