基于有限环上多项式的数字电路形式验证方法

论文摘要

随着集成电路的规模变得越来越大、功能越来越复杂，功能验证已经成为设计流程的主要瓶颈。据统计，设计验证的时间已占到整个设计周期的一半以上。传统的基于模拟的验证方法不但需要花费大量的时间，而且不能保证完全的验证覆盖率，己经不能满足现时集成电路设计的要求。形式验证利用数学的方法隐式遍历所有可能的情况，能保证完全的验证覆盖率，所需要的验证时间也大幅减少，是克服验证瓶颈的可行途径。本文以有限环上多项式为基础模型，围绕算术密集型设计(例如数字信号处理(DSP)电路)的等价性检验和定界模型检验，进行了深入研究，取得了如下创新性成果：(1)针对实现多项式运算的定点数据通路的逻辑门级与寄存器传输级(RTL)之间的等价性检验，提出一种将定点数据通路的位级描述抽象为字级描述的方法。首先采用算术转换描述定点数据通路的逻辑门级功能，采用多项式函数描述定点数据通路的RTL功能，然后采用牛顿插值方法迭代地将算术转换抽象为多项式函数，以实现定点数据通路的逻辑门级模型与RTL模型之间的等价性检验。实验结果表明，该方法的速度与已有方法相比对乘法器的验证平均要快1至2倍，对一些实现多项式运算的定点数据通路的验证平均要快1个数量级。(2)针对定点数据通路的设计规范与RTL实现或优化后的RTL实现之间的等价性检验，构建vanishing多项式环的理想的极小强Gr(o|¨)bner基，并在此基础上提出一种高效的等价性检验算法。通过使用多项式函数建模定点数据通路的设计规范和RTL实现，将等价性检验问题转化为判断一个多项式函数是否为vanishing多项式的问题，进而采用vanishing多项式环的理想的极小强Gr(o|¨)bner基来有效地解决该问题。理论分析表明该算法的时间复杂度的上界比已有方法的时间复杂度的上界小。实验结果表明，对一些实现多项式运算的定点数据通路的等价性检验，该方法比已有方法平均要快2倍。(3)针对DSP电路的高层次设计验证的定界模型检验，提出一种基于有限环上多项式理想的Gr(o|¨)bner基的定界模型检验方法。通过使用有限环上多项式等式建模高层次设计和待验证性质，将定界模型检验问题转化为定理证明问题，并采用有限环上多项式理想的Gr(o|¨)bner基有效地解决该定理证明问题。实验结果表明，与基于布尔可满足性(SAT)和基于线性规划的RTL SAT的定界模型检验方法相比，该方法对一些DSP电路的验证平均要快1倍到1个数量级。

论文目录

• 摘要
• Abstract
• 第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 本章小结
• 结论
• 参考文献
• 攻读博士学位期间发表的论文和取得的科研成果
• 致谢