文摘
英文文摘
声明
第1章绪论
1.1课题的背景及意义
1.2研究现状
1.3本文的工作
1.4论文的组织结构
第2章集成电路的形式验证综述
2.1形式验证的数学基础
2.1.1基于正则的判决图的形式验证
2.1.2基于SAT的形式验证
2.2形式验证方法
2.2.1等价性检验
2.2.2模型检验
2.2.3定理证明
2.3本章小结
第3章算术转换到多项式函数的抽象
3.1引言
3.2算术转换和多项式函数
3.2.1算术转换
3.2.2多项式函数
3.3 AT到多项式的抽象
3.3.1对于一元多项式的抽象
3.3.2对于多元多项式的抽象
3.4实验结果
3.5本章小结
第4章基于vanishing多项式的等价性检验方法
4.1引言
4.2 vanishing多项式环的理想
4.3定点数据通路的等价性检验
4.4实验结果
4.5本章小结
第5章基于有限环上多项式的定界模型检验方法
5.1引言
5.2有限环上多项式理想的Gr(o)bner基
5.3电路设计的多项式表示
5.3.1算术运算部件
5.3.2布尔逻辑
5.3.3多路选择器
5.3.4寄存器
5.3.5其他运算
5.4性质描述
5.5基于有限环上多项式理想的Gr(o)bner基的定界模型检验
5.5.1电路展开
5.5.2从待验证性质的前件产生有限环上多项式等式集合
5.5.3从待验证性质的后件产生有限环上多项式等式集合
5.5.4采用有限环上多项式理想的Gr(O)bner基解决定理证明问题
5.5.5求解反例
5.6实验结果
5.7本章小结
结 论
参考文献
攻读博士学位期间发表的论文和取得的科研成果
致 谢