集成电路的逻辑等价性验证研究
| 摘要 | 第1-6页 |
| Abstract | 第6-14页 |
| 第1章 绪论 | 第14-22页 |
| ·论文背景及意义 | 第14-18页 |
| ·论文的主要工作与创新点 | 第18-20页 |
| ·论文的组织结构 | 第20-22页 |
| 第2章 集成电路设计验证综述 | 第22-32页 |
| ·验证方法分类 | 第22-26页 |
| ·软件模拟 | 第22-24页 |
| ·硬件仿真 | 第24页 |
| ·形式验证 | 第24-25页 |
| ·半形式化验证 | 第25-26页 |
| ·形式化验证方法分类 | 第26-30页 |
| ·等价性验证 | 第27-29页 |
| ·定理证明 | 第29-30页 |
| ·模型检验 | 第30页 |
| ·本章小结 | 第30-32页 |
| 第3章 二叉判定图及其在等价性验证中的应用 | 第32-46页 |
| ·二叉判定图相关的定义 | 第32-35页 |
| ·基本的二叉判定图 | 第32-34页 |
| ·有序二叉判定图 | 第34-35页 |
| ·精简的有序二叉判定图 | 第35页 |
| ·二叉判定图的性质 | 第35-36页 |
| ·电路的二叉判定图表示 | 第36-37页 |
| ·二叉判定图的运算 | 第37-41页 |
| ·二叉判定图的迭代运算 | 第37-38页 |
| ·基于ite的二叉判定图运算 | 第38-41页 |
| ·二叉判定图的变量排序 | 第41-44页 |
| ·变量排序对二叉判定图的影响 | 第41-42页 |
| ·启发式变量排序 | 第42-43页 |
| ·动态变量排序 | 第43-44页 |
| ·本章小结 | 第44-46页 |
| 第4章 基于BDD的组合电路等价性验证 | 第46-63页 |
| ·功能性等价验证 | 第46-47页 |
| ·结构性等价验证 | 第47-53页 |
| ·基于替代的结构性验证方法 | 第48-51页 |
| ·基于学习的结构性验证方法 | 第51-52页 |
| ·基于转换的结构性验证方法 | 第52-53页 |
| ·结合通用割集和专用割集的等价性验证方法 | 第53-61页 |
| ·结合通用割集和专用割集的验证流程 | 第54-57页 |
| ·对专用割集依赖性的处理 | 第57-59页 |
| ·实验结果及分析 | 第59-61页 |
| ·本章小结 | 第61-63页 |
| 第5章 基于BDD的时序电路等价性验证 | 第63-82页 |
| ·时序电路的数学模型表示 | 第63-64页 |
| ·基于状态遍历的时序等价性验证 | 第64-70页 |
| ·时序电路的联接电路miter | 第64-65页 |
| ·时序电路的显式状态遍历及等价性验证 | 第65-66页 |
| ·基于BDD的隐式状态遍历及等价性验证 | 第66-70页 |
| ·基于寄存器匹配的时序等价性验证 | 第70-72页 |
| ·用迭代的方法进行寄存器匹配 | 第70-71页 |
| ·用先假设再证明的方法进行寄存器匹配 | 第71-72页 |
| ·利用状态缓存的时序等价性验证方法 | 第72-80页 |
| ·通过功能模拟缓存可达状态 | 第73-74页 |
| ·在简化的联接电路中提炼可达状态 | 第74-75页 |
| ·在简化的联接电路中验证寄存器的等价性 | 第75-78页 |
| ·对原始输出的验证及内部等价点在验证过程中的应用 | 第78页 |
| ·实验结果及分析 | 第78-80页 |
| ·本章小结 | 第80-82页 |
| 第6章 基于BDD和SAT的时序电路等价性验证 | 第82-102页 |
| ·有关可满足性问题的基本定义 | 第82-83页 |
| ·求解布尔可满足性问题的算法 | 第83-90页 |
| ·布尔可满足性问题的算法分类 | 第83-84页 |
| ·DPLL算法 | 第84-90页 |
| ·电路问题的可满足性求解 | 第90-95页 |
| ·逻辑门的CNF格式表示 | 第90-91页 |
| ·SAT解算器在电路问题中的应用 | 第91-95页 |
| ·结合BDD和SAT的时序验证方法 | 第95-100页 |
| ·结合BDD和SAT的时序验证流程 | 第95-97页 |
| ·实验结果与分析 | 第97-100页 |
| ·本章小结 | 第100-102页 |
| 第7章 总结与展望 | 第102-106页 |
| ·论文工作总结 | 第102-104页 |
| ·下一步工作展望 | 第104-106页 |
| 参考文献 | 第106-117页 |
| 攻读学位期间发表/录用的学术论文 | 第117-118页 |
| 致谢 | 第118页 |
