形式化验证技术在EDA软件开发中的应用

论文摘要

形式化验证技术起源于20世纪60年代软件危机。直至整个70年代，形式化验证技术所针对的一般是转换型程序，即单纯进行科学计算、计数等功能的软件。形式化验证的巨大成功首先来自于80年代后期符号模型检验(Symbolic ModelChecking)方法的提出和在硬件验证中的实现。1987年，McMillan在博士论文中，首次将发表于前一年的二分决策图(Binary Decision Diagram)技术应用于模型检验中，从而大大地缓解了空间爆炸问题。其后的一系列改进更增强了对符号模型检验技术的信心。然而，人们很快就发现，对于复杂系统，空间爆炸问题仍是符号模型检验技术难以克服的障碍，这导致了在1999年定界模型检验技术的提出。总的来说，模型检验方法在硬件验证上是成功的，其根本原因是硬件通常有层次性且比较规整，相比于软件的复杂程序结构，更易于描述和验证。本文主要介绍形式化验证技术在集成电路自动化设计中的应用。首先介绍了形式化验证技术的发展现状和集成电路自动化设计流程，然后介绍了框架时序逻辑程序设计语言，本文利用这种语言实现了简单时序电路的描述。随后本文介绍了模型检验工具的设计原理和移植框架，并使用移植后的模型检验工具对采用框架时序逻辑程序设计语言描述的电路进行模拟验证。最后本文介绍了可满足性验证和等价性验证。本文详细阐述了集成电路自动化设计中的逻辑综合过程，设计原则，综合工具，并在此基础上完成了组合电路逻辑综合前后的等价性验证。

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 研究背景
• 1.2 基于 HDL 的 FPGA 设计流程
• 1.2.1 设计输入
• 1.2.2 功能仿真
• 1.2.3 综合优化
• 1.2.4 综合后仿真
• 1.2.5 布局布线
• 1.2.6 布局布线后仿真
• 1.2.7 生成并下载位流文件
• 1.3 形式化验证
• 1.4 本文研究内容和章节安排
• 第二章 时序逻辑及框架时序逻辑程序设计语言
• 2.1 时序逻辑
• 2.2 框架时序逻辑程序设计语言
• 2.3 本章小结
• 第三章 解释器工具移植开发及应用
• 3.1 解释器设计原理
• 3.2 解释器移植
• 3.2.1 QT 简介
• 3.2.2 解释器移植框架
• 3.3 设计简单时序电路
• 3.3.1 触发器电路
• 3.3.2 使用框架时序逻辑语言描述触发器元件
• 3.3.3 寄存器电路
• 3.3.4 使用框架时序逻辑语言设计寄存器电路
• 3.4 本章小结
• 第四章 可满足性验证
• 4.1 可满足性验证
• 4.1.1 布尔公式
• 4.1.2 消解和相融
• 4.2 SAT 算法
• 4.2.1 DP 算法
• 4.2.2 DPLL 算法
• 4.3 DPLL 算法改进
• 4.3.1 基本流程
• 4.3.2 启发分支
• 4.3.3 决策推理
• 4.3.4 基于冲突的学习和非同步回溯
• 4.3.5 预处理、重启及其它技术
• 4.3.6 学习子句的删除
• 4.3.7 基准电路测试
• 4.4 本章小结
• 第五章 组合电路的等价性验证
• 5.1 逻辑综合
• 5.1.1 约束条件
• 5.1.2 基本流程
• 5.1.3 逻辑综合工具
• 5.1.4 RTL 设计原则
• 5.2 逻辑综合前后电路等价性
• 5.3 本章小结
• 总结与展望
• 致谢
• 参考文献
• 研究成果