RTL到门级设计的等价性验证的研究
| 摘要 | 第1-5页 |
| Abstract | 第5-12页 |
| 第1章 绪论 | 第12-25页 |
| ·课题背景 | 第12-14页 |
| ·研究现状 | 第14-22页 |
| ·等价性验证的研究现状 | 第14-16页 |
| ·综合引擎的研究现状 | 第16-18页 |
| ·算术电路等价性验证的研究现状 | 第18-22页 |
| ·论文的主要工作和创新点 | 第22-23页 |
| ·论文的组织结构 | 第23-25页 |
| 第2章 ZDFV的综合引擎的设计与实现 | 第25-45页 |
| ·综合技术简述 | 第25-27页 |
| ·综合引擎在验证系统中的位置 | 第27-28页 |
| ·可综合的Verilog描述子集 | 第28-31页 |
| ·变量声明和使用 | 第29页 |
| ·连续赋值语句 | 第29页 |
| ·过程赋值语句 | 第29-30页 |
| ·串行语句块 | 第30页 |
| ·高级程序语句 | 第30-31页 |
| ·Icarus Verilog的实现 | 第31-35页 |
| ·预处理 | 第32页 |
| ·初步解析(parse) | 第32-33页 |
| ·精解析(elaborate) | 第33页 |
| ·综合优化(synthesis) | 第33-34页 |
| ·代码生成 | 第34-35页 |
| ·对Icarus Verilog的改进 | 第35-40页 |
| ·增加对高级程序语句的支持 | 第35-40页 |
| ·提高综合引擎的通用性 | 第40页 |
| ·采取多种手段提高运行效率 | 第40页 |
| ·ZDFV综合引擎的实现 | 第40-42页 |
| ·实验数据 | 第42-44页 |
| ·小结 | 第44-45页 |
| 第3章 提高电路相似性的算法研究 | 第45-56页 |
| ·组合电路等价性验证方法概述 | 第45-50页 |
| ·功能等价性验证方法 | 第45-46页 |
| ·增量等价性验证方法 | 第46-50页 |
| ·面向通用模块的相似性算法 | 第50-54页 |
| ·综合优化对电路结构的影响 | 第50-52页 |
| ·算法实现细节及复杂度分析 | 第52-54页 |
| ·实验结果 | 第54页 |
| ·小结 | 第54-56页 |
| 第4章 数据通路的等价性验证 | 第56-67页 |
| ·数据通路的等价性研究现状 | 第56-57页 |
| ·算法模型和定理 | 第57-60页 |
| ·算符排序算法 | 第60-63页 |
| ·距离计算 | 第60-61页 |
| ·初始变量分组 | 第61-62页 |
| ·乘数被乘数的识别 | 第62-63页 |
| ·验证框架 | 第63页 |
| ·实例分析 | 第63-65页 |
| ·小结 | 第65-67页 |
| 第5章 结合HAG的算术单元等价性验证 | 第67-80页 |
| ·算术单元等价性验证的研究现状 | 第67-71页 |
| ·算法模型和定义 | 第71-72页 |
| ·电路实现方案提取算法 | 第72-77页 |
| ·HAG提取算法 | 第73-74页 |
| ·加法树构架提取 | 第74-76页 |
| ·乘法编码方式识别 | 第76-77页 |
| ·结合HAG的算术电路验证 | 第77-78页 |
| ·测试结果与分析 | 第78-79页 |
| ·小结 | 第79-80页 |
| 第6章 基于混合SAT引擎的RTL验证算法 | 第80-99页 |
| ·布尔逻辑的SAT引擎 | 第80-87页 |
| ·电路布尔逻辑的SAT模型 | 第80-81页 |
| ·布尔逻辑的SAT引擎 | 第81-87页 |
| ·混合SAT引擎求解电路问题 | 第87-93页 |
| ·混合SAT引擎的研究现状 | 第87-88页 |
| ·HDPLL算法 | 第88-93页 |
| ·基于混合SAT引擎的RTL验证系统 | 第93-97页 |
| ·实现细节 | 第94-96页 |
| ·实验数据 | 第96-97页 |
| ·小结 | 第97-99页 |
| 第7章 结论与展望 | 第99-103页 |
| ·论文工作小结 | 第99-102页 |
| ·下一步工作展望 | 第102-103页 |
| 参考文献 | 第103-114页 |
| 致谢 | 第114-115页 |
| 附录 1: Bench文件语法 | 第115-118页 |
| 附录 2: 攻读学位期间发表/录用的学术论文 | 第118页 |
