| 致谢 | 第1-6页 |
| 中文摘要 | 第6-7页 |
| ABSTRACT | 第7-10页 |
| 1 引言 | 第10-18页 |
| ·EDA技术的发展 | 第10-12页 |
| ·研究背景及意义 | 第12-16页 |
| ·本文的工作 | 第16页 |
| ·本文的结构 | 第16-18页 |
| 2 形式化验证技术 | 第18-26页 |
| ·模型检验方法 | 第18-23页 |
| ·模型检验理论基础 | 第18-21页 |
| ·显式模型检验 | 第21页 |
| ·符号模型检验 | 第21-22页 |
| ·定界模型检验 | 第22-23页 |
| ·无界模型检验 | 第23页 |
| ·等价验证方法 | 第23-25页 |
| ·组合等价验证 | 第23-24页 |
| ·时序等价验证 | 第24-25页 |
| ·本章小结 | 第25-26页 |
| 3 电路形式化验证的数学方法 | 第26-53页 |
| ·正则判决图方法 | 第26-33页 |
| ·二元判决图方法BDD | 第26-28页 |
| ·字级判决图方法WLDD | 第28-31页 |
| ·TED方法 | 第31-32页 |
| ·各类判决图方法的总结以及复杂度比较 | 第32-33页 |
| ·代数方法 | 第33-52页 |
| ·可满足性问题SAT | 第33-35页 |
| ·约束满足问题CSP | 第35-39页 |
| ·多项式符号代数PSA | 第39-50页 |
| ·代数方法之间的关系及求解能力比较 | 第50-52页 |
| ·本章小结 | 第52-53页 |
| 4 基于多项式符号代数方法的电路等价验证 | 第53-67页 |
| ·电路的多项式集合建模 | 第53-58页 |
| ·高层次数据通路 | 第53-54页 |
| ·高层次数据通路的多项式集合表示 | 第54-58页 |
| ·基于吴方法及Groebner基的高层次数据通路等价验证方法 | 第58-66页 |
| ·定义功能等价 | 第58-60页 |
| ·等价验证问题求解 | 第60-63页 |
| ·实例验证 | 第63-66页 |
| ·本章小结 | 第66-67页 |
| 5 总结与展望 | 第67-69页 |
| ·总结 | 第67-68页 |
| ·展望 | 第68-69页 |
| 参考文献 | 第69-72页 |
| 作者简历 | 第72-74页 |
| 学位论文数据集 | 第74页 |