本文關(guān)鍵詞：基于FPGA鏌擬的SAT求解方法，，由筆耕文化傳播整理發(fā)布。

【摘要】：集成電路設(shè)計(jì)的復(fù)雜程度和設(shè)計(jì)規(guī)模呈指數(shù)增長(zhǎng),驗(yàn)證技術(shù)已經(jīng)成為整個(gè)集成電路設(shè)計(jì)領(lǐng)域的瓶頸,利用BDD技術(shù)的形式驗(yàn)證方法在面對(duì)小規(guī)模以及中等規(guī)模電路時(shí)能夠顯示出優(yōu)勢(shì),大規(guī)模電路呈指數(shù)增長(zhǎng)的情況下并不適用。隨著近些年計(jì)算機(jī)領(lǐng)域研究者對(duì)可滿足性問題的深入研究并取得巨大進(jìn)展,使得實(shí)踐和理論當(dāng)中的很多之前無(wú)法解決的問題能夠轉(zhuǎn)化為SAT問題后再進(jìn)行解決。但以zChaff、DPLL等求解可滿足問題的算法程序?yàn)榛A(chǔ)的軟件SAT求解器對(duì)大規(guī)模電路以及特定領(lǐng)域問題效果不佳。本文采用硬件模擬的辦法來(lái)求解SAT問題,將SAT問題映射為現(xiàn)場(chǎng)可編程門陣列(FPGA)芯片,由FPGA芯片自主求解此問題。具體而言,我們研究了針對(duì)實(shí)際系統(tǒng)的CNF公式實(shí)例,自動(dòng)化地定制編譯和轉(zhuǎn)換為FPGA芯片,由這種SAT求解芯片自主求解SAT問題的技術(shù)。論文中提出的流程構(gòu)成了一個(gè)從CNF公式到電路的轉(zhuǎn)換、FPGA芯片仿真、綜合、驗(yàn)證、配置、下載和自主驗(yàn)證的統(tǒng)一框架,可以方便快速判斷CNF式是否可滿足,在自動(dòng)化設(shè)計(jì)分析與驗(yàn)證領(lǐng)域具有深遠(yuǎn)意義。
【關(guān)鍵詞】：布爾可滿足 現(xiàn)場(chǎng)可編程門陣列 合取范式 形式驗(yàn)證方法
【學(xué)位授予單位】：廣西民族大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2016
【分類號(hào)】：TN402;TN791
【目錄】：

• 摘要3-4
• ABSTRACT4-8
• 1 緒論8-13
• 1.1 研究意義8
• 1.2 研究背景8-9
• 1.3 論文的相關(guān)工作9-11
• 1.3.1 論文的主要工具10
• 1.3.2 論文的主要工作內(nèi)容10-11
• 1.4 論文的結(jié)構(gòu)安排11-13
• 2 SAT問題與電路13-21
• 2.1 集成電路的設(shè)計(jì)驗(yàn)證13-14
• 2.1.1 模擬驗(yàn)證方法13-14
• 2.1.2 形式驗(yàn)證方法14
• 2.2 電路形式化驗(yàn)證與SAT14-19
• 2.2.1 布爾可滿足問題15
• 2.2.2 合取范式的表示方法15-17
• 2.2.3 CNF電路生成算法17-19
• 2.2.3.1 硬件描述語(yǔ)言語(yǔ)法結(jié)構(gòu)17-18
• 2.2.3.2 Verilog的設(shè)計(jì)流程18-19
• 2.3 基于電路的SAT求解方法19-21
• 2.3.1 應(yīng)用型算法20
• 2.3.2 實(shí)例型算法20-21
• 3 支持可編程和快速部署的FPGA芯片21-31
• 3.1 選用FPGA芯片21-22
• 3.2 FPGA的內(nèi)部結(jié)構(gòu)：22-26
• 3.3 VC707簡(jiǎn)介26-27
• 3.4 利用ISE的FPGA開發(fā)27-29
• 3.5 可編程邏輯器件FPGA的配置29-31
• 4 自主計(jì)算的實(shí)例型SAT芯片設(shè)計(jì)31-37
• 4.1 SAT問題的翻譯31-34
• 4.1.1 CNF公式到電路圖的轉(zhuǎn)化32-33
• 4.1.2 CNF公式翻譯算法33-34
• 4.2 SAT問題的封裝34-35
• 4.2.1 CNF模塊34
• 4.2.2 激勵(lì)模塊34-35
• 4.3 FPGA實(shí)現(xiàn)35-37
• 5 實(shí)例型SAT芯片的實(shí)現(xiàn)與仿真37-41
• 5.1 測(cè)試平臺(tái)37
• 5.2 實(shí)驗(yàn)方案37
• 5.3 RTL實(shí)驗(yàn)原理圖37-39
• 5.4 實(shí)驗(yàn)結(jié)果39-41
• 6 總結(jié)與展望41-43
• 6.1 全文工作總結(jié)41
• 6.2 研究展望41-43
• 參考文獻(xiàn)43-47
• 附錄147-49
• 附錄249-52
• 致謝52-53
• 攻讀碩士期間參與的科研項(xiàng)目53-54
• 攻讀碩士期間發(fā)表的學(xué)術(shù)論文54

【相似文獻(xiàn)】

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

1 陳麗;高巍巍;;形式驗(yàn)證方法綜述[J];大視野;2008年07期

2 王彬,任艷穎,林爭(zhēng)輝;事務(wù)級(jí)形式驗(yàn)證技術(shù)及8051驗(yàn)證模型[J];計(jì)算機(jī)輔助設(shè)計(jì)與圖形學(xué)學(xué)報(bào);2003年08期

3 高新巖;吳盡昭;閆煒;周寧;;非經(jīng)典切片技術(shù)及其在形式驗(yàn)證中的應(yīng)用綜述[J];計(jì)算機(jī)工程與應(yīng)用;2007年36期

4 葉新銘;;軟件形式驗(yàn)證與測(cè)試集成方法研究綜述[J];內(nèi)蒙古大學(xué)學(xué)報(bào)(自然科學(xué)版);2009年04期

5 方敏;張雅順;李輝;;混合系統(tǒng)的形式驗(yàn)證方法[J];系統(tǒng)仿真學(xué)報(bào);2006年10期

6 徐亮;劉宏;;實(shí)用模型的自動(dòng)化形式驗(yàn)證[J];湖南大學(xué)學(xué)報(bào)(自然科學(xué)版);2013年09期

7 方佳結(jié),章開和,唐璞山;基于重寫規(guī)則法的形式驗(yàn)證技術(shù)[J];固體電子學(xué)研究與進(jìn)展;1988年04期

8 羅來(lái)豹;方敏;劉震;;形式驗(yàn)證中近似流管道的算法研究[J];合肥工業(yè)大學(xué)學(xué)報(bào)(自然科學(xué)版);2010年10期

9 游余新;;基于屬性的形式驗(yàn)證技術(shù)及應(yīng)用[J];中國(guó)集成電路;2013年12期

10 張學(xué)軍,謝劍英,張苗苗;混合系統(tǒng)的形式驗(yàn)證技術(shù)及其在化工過程控制中的應(yīng)用[J];控制與決策;2001年02期

中國(guó)重要會(huì)議論文全文數(shù)據(jù)庫(kù) 前3條

1 李春明;宋新亮;;代碼風(fēng)格所引起形式驗(yàn)證失配問題的分析[A];第五屆中國(guó)測(cè)試學(xué)術(shù)會(huì)議論文集[C];2008年

2 韓俊剛;吳為民;李暾;杜慧敏;;(A7)專題討論2:形式驗(yàn)證與模擬驗(yàn)證[A];第四屆中國(guó)測(cè)試學(xué)術(shù)會(huì)議論文集[C];2006年

3 李光輝;邵明;李曉維;;用形式方法驗(yàn)證通用CPU設(shè)計(jì)[A];第十屆全國(guó)容錯(cuò)計(jì)算學(xué)術(shù)會(huì)議論文集[C];2003年

中國(guó)博士學(xué)位論文全文數(shù)據(jù)庫(kù) 前6條

1 盧永江;超大規(guī)模集成電路形式驗(yàn)證的方法研究[D];浙江大學(xué);2005年

2 吳俊華;VLSI設(shè)計(jì)中的形式驗(yàn)證方法研究[D];哈爾濱工程大學(xué);2009年

3 楊志;基于多項(xiàng)式符號(hào)代數(shù)的數(shù)字電路形式驗(yàn)證方法研究[D];哈爾濱工程大學(xué);2009年

4 李東海;基于有限環(huán)上多項(xiàng)式的數(shù)字電路形式驗(yàn)證方法[D];哈爾濱工程大學(xué);2008年

5 范德會(huì);基于PSA的集成電路形式驗(yàn)證方法研究[D];哈爾濱工程大學(xué);2012年

6 王秀芹;基于SAT的數(shù)字電路形式驗(yàn)證方法研究[D];哈爾濱工程大學(xué);2009年

中國(guó)碩士學(xué)位論文全文數(shù)據(jù)庫(kù) 前10條

1 張波;基于SOC異步FIFO的設(shè)計(jì)與形式驗(yàn)證[D];西安電子科技大學(xué);2015年

2 毛樂樂;基于FPGA鏌擬的SAT求解方法[D];廣西民族大學(xué);2016年

3 朱學(xué)仕;形式驗(yàn)證技術(shù)的應(yīng)用研究[D];哈爾濱工程大學(xué);2004年

4 李健;形式驗(yàn)證技術(shù)中流管道近似方法的研究與應(yīng)用[D];合肥工業(yè)大學(xué);2009年

5 張雅順;混合系統(tǒng)的形式驗(yàn)證方法及其應(yīng)用[D];合肥工業(yè)大學(xué);2006年

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

7 呂向東;形式驗(yàn)證在SOC設(shè)計(jì)中的應(yīng)用研究[D];西安電子科技大學(xué);2009年

8 張望;數(shù)字電路后端的形式驗(yàn)證方法研究及應(yīng)用[D];西安電子科技大學(xué);2008年

9 古進(jìn);超大規(guī)模集成電路設(shè)計(jì)流程中的驗(yàn)證技術(shù)及實(shí)踐[D];浙江大學(xué);2004年

10 張斌;混合系統(tǒng)形式驗(yàn)證中的問題研究[D];合肥工業(yè)大學(xué);2007年

  本文關(guān)鍵詞：基于FPGA鏌擬的SAT求解方法，由筆耕文化傳播整理發(fā)布。

本文編號(hào)：267978