论文部分内容阅读
随着集成电路的规模变得越来越大、功能越来越复杂，功能验证已经成为设计流程的主要瓶颈。据统计，设计验证的时间已占到整个设计周期的一半以上。传统的基于模拟的验证方法不但需要花费大量的时间，而且不能保证完全的验证覆盖率，己经不能满足现时集成电路设计的要求。形式验证利用数学的方法隐式遍历所有可能的情况，能保证完全的验证覆盖率，所需要的验证时间也大幅减少，是克服验证瓶颈的可行途径。本文以有限环上多项式为基础模型，围绕算术密集型设计(例如数字信号处理(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个数量级。