基于FPGA镆拟的SAT求解方法

发布时间：2017-03-26 00:09

  本文关键词：基于FPGA镆拟的SAT求解方法，，由笔耕文化传播整理发布。

【摘要】：集成电路设计的复杂程度和设计规模呈指数增长,验证技术已经成为整个集成电路设计领域的瓶颈,利用BDD技术的形式验证方法在面对小规模以及中等规模电路时能够显示出优势,大规模电路呈指数增长的情况下并不适用。随着近些年计算机领域研究者对可满足性问题的深入研究并取得巨大进展,使得实践和理论当中的很多之前无法解决的问题能够转化为SAT问题后再进行解决。但以zChaff、DPLL等求解可满足问题的算法程序为基础的软件SAT求解器对大规模电路以及特定领域问题效果不佳。本文采用硬件模拟的办法来求解SAT问题,将SAT问题映射为现场可编程门阵列(FPGA)芯片,由FPGA芯片自主求解此问题。具体而言,我们研究了针对实际系统的CNF公式实例,自动化地定制编译和转换为FPGA芯片,由这种SAT求解芯片自主求解SAT问题的技术。论文中提出的流程构成了一个从CNF公式到电路的转换、FPGA芯片仿真、综合、验证、配置、下载和自主验证的统一框架,可以方便快速判断CNF式是否可满足,在自动化设计分析与验证领域具有深远意义。
【关键词】：布尔可满足 现场可编程门阵列 合取范式 形式验证方法
【学位授予单位】：广西民族大学
【学位级别】：硕士
【学位授予年份】：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开发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实现35-37
• 5 实例型SAT芯片的实现与仿真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
• 攻读硕士期间发表的学术论文54

【相似文献】

中国期刊全文数据库 前10条

1 陈丽;高巍巍;;形式验证方法综述[J];大视野;2008年07期

2 王彬,任艳颖,林争辉;事务级形式验证技术及8051验证模型[J];计算机辅助设计与图形学学报;2003年08期

3 高新岩;吴尽昭;闫炜;周宁;;非经典切片技术及其在形式验证中的应用综述[J];计算机工程与应用;2007年36期

4 叶新铭;;软件形式验证与测试集成方法研究综述[J];内蒙古大学学报(自然科学版);2009年04期

5 方敏;张雅顺;李辉;;混合系统的形式验证方法[J];系统仿真学报;2006年10期

6 徐亮;刘宏;;实用模型的自动化形式验证[J];湖南大学学报(自然科学版);2013年09期

7 方佳结,章开和,唐璞山;基于重写规则法的形式验证技术[J];固体电子学研究与进展;1988年04期

8 罗来豹;方敏;刘震;;形式验证中近似流管道的算法研究[J];合肥工业大学学报(自然科学版);2010年10期

9 游余新;;基于属性的形式验证技术及应用[J];中国集成电路;2013年12期

10 张学军,谢剑英,张苗苗;混合系统的形式验证技术及其在化工过程控制中的应用[J];控制与决策;2001年02期

中国重要会议论文全文数据库 前3条

1 李春明;宋新亮;;代码风格所引起形式验证失配问题的分析[A];第五届中国测试学术会议论文集[C];2008年

2 韩俊刚;吴为民;李暾;杜慧敏;;(A7)专题讨论2:形式验证与模拟验证[A];第四届中国测试学术会议论文集[C];2006年

3 李光辉;邵明;李晓维;;用形式方法验证通用CPU设计[A];第十届全国容错计算学术会议论文集[C];2003年

中国博士学位论文全文数据库 前6条

1 卢永江;超大规模集成电路形式验证的方法研究[D];浙江大学;2005年

2 吴俊华;VLSI设计中的形式验证方法研究[D];哈尔滨工程大学;2009年

3 杨志;基于多项式符号代数的数字电路形式验证方法研究[D];哈尔滨工程大学;2009年

4 李东海;基于有限环上多项式的数字电路形式验证方法[D];哈尔滨工程大学;2008年

5 范德会;基于PSA的集成电路形式验证方法研究[D];哈尔滨工程大学;2012年

6 王秀芹;基于SAT的数字电路形式验证方法研究[D];哈尔滨工程大学;2009年

中国硕士学位论文全文数据库 前10条

1 张波;基于SOC异步FIFO的设计与形式验证[D];西安电子科技大学;2015年

2 毛乐乐;基于FPGA镆拟的SAT求解方法[D];广西民族大学;2016年

3 朱学仕;形式验证技术的应用研究[D];哈尔滨工程大学;2004年

4 李健;形式验证技术中流管道近似方法的研究与应用[D];合肥工业大学;2009年

5 张雅顺;混合系统的形式验证方法及其应用[D];合肥工业大学;2006年

6 吴俊华;组合电路的形式验证方法研究[D];哈尔滨工程大学;2004年

7 吕向东;形式验证在SOC设计中的应用研究[D];西安电子科技大学;2009年

8 张望;数字电路后端的形式验证方法研究及应用[D];西安电子科技大学;2008年

9 古进;超大规模集成电路设计流程中的验证技术及实践[D];浙江大学;2004年

10 张斌;混合系统形式验证中的问题研究[D];合肥工业大学;2007年

  本文关键词：基于FPGA镆拟的SAT求解方法，由笔耕文化传播整理发布。

本文编号：267978