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

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

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

【相似文獻】

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

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

2 王彬,任艷穎,林爭輝;事務級形式驗證技術及8051驗證模型[J];計算機輔助設計與圖形學學報;2003年08期

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

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

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

6 徐亮;劉宏;;實用模型的自動化形式驗證[J];湖南大學學報(自然科學版);2013年09期

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

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

9 游余新;;基于屬性的形式驗證技術及應用[J];中國集成電路;2013年12期

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

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

1 李春明;宋新亮;;代碼風格所引起形式驗證失配問題的分析[A];第五屆中國測試學術會議論文集[C];2008年

2 韓俊剛;吳為民;李暾;杜慧敏;;(A7)專題討論2:形式驗證與模擬驗證[A];第四屆中國測試學術會議論文集[C];2006年

3 李光輝;邵明;李曉維;;用形式方法驗證通用CPU設計[A];第十屆全國容錯計算學術會議論文集[C];2003年

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

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

2 吳俊華;VLSI設計中的形式驗證方法研究[D];哈爾濱工程大學;2009年

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

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

5 范德會;基于PSA的集成電路形式驗證方法研究[D];哈爾濱工程大學;2012年

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

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

1 張波;基于SOC異步FIFO的設計與形式驗證[D];西安電子科技大學;2015年

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

3 朱學仕;形式驗證技術的應用研究[D];哈爾濱工程大學;2004年

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

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

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

7 呂向東;形式驗證在SOC設計中的應用研究[D];西安電子科技大學;2009年

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

9 古進;超大規(guī)模集成電路設計流程中的驗證技術及實踐[D];浙江大學;2004年

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

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

本文編號：267978