运算电路的形式化验证方法研究

发布时间：2020-05-31 19:56

【摘要】：运算电路模块是当代微处理器的关键组件。微处理器电路设计的验证工作必须确保运算电路模块设计的正确性。当电路复杂度达到一定规模后，传统的仿真验证方法已无法覆盖整个状态空间，从而无法保证像微处理器运算电路这类复杂设计的正确性。因此，基于形式化方法的运算电路验证方法，特别是完全自动化的模型检验方法，已经成为当前国内外科研机构以及EDA厂商所关注的热点问题。本文结合龙芯I号微处理器运算部件的设计和验证工作，系统地研究了运算电路的规范语言、基于决策图的模型检验方法以及基于可满足性判定的模型检验方法。以下是本文的主要贡献与创新点： (1)定义了运算电路CTL公式的语法和语义，给出了运算电路CTL公式的模型检验方法以及基于~*PHDD的实现方法。 (2)提出了基于~*PHDD实现运算操作算法的一般优化原则。特别地，针对运算电路验证中经常出现的基为2的整数次幂的整除和取模运算，推出了四条定理，并且基于这四条定理对运算过程进行了简化。这些措施有效提高了~*PHDD运算操作算法的效率。 (3)提出了更接近于实际取值范围的~*PHDD上下界计算算法。在整除、取模以及比较运算中，上下界可用于简化运算操作。当函数上下界越接近~*PHDD实际取值范围时，满足简化条件的可能性越大，简化算法越有效。 (4)提出了基于条件预处理的条件约束算法，降低了条件约束算法的运行时间；同时又提出了多级约束机制和约束过滤机制，降低了约束条件的规模，并消除了大量非必要的约束函数调用。 (5)提出了基于可满足性判定算法的运算电路验证方法，突破了现有可满足性判定算法在应用上的局限性。实验结果表明，该验证方法对于存在设计错误的运算电路或者约束严格的正确运算电路非常有效，是决策图方法的一个有效补充。 (6)基于上述研究结果，，实现了一个字级模型检验系统ArithSMV，并使用该系统验证了龙芯I号微处理器的浮点加法部件。实验证明该系统具有实用高效的特点。
【图文】：

ASIC设计,比重,摩尔定律,集成电路

当前摩尔定律的定义。按照摩尔定律，2010年微处理器包含的晶体管数将达到18亿个。工艺水平的提高使单个芯片中可集成的功能部件逐渐增多，随着芯片设计越来越复杂，验证工作在整个芯片设计中所占的比重也越来越大。如图1.1所示，2003年，在100万逻辑门的SOC设计中，仿真验证工作在整个设计工作量中的比重达到50一80%D[503]，即项目中有超过一半的设计资源包括计算机和人力资源都在致力于设计验证工作。因此，随着集成电路复杂度的增加，功能验证已经成为集成电路开发过程中的瓶颈，对验证方法进行深入研究将有助于缩短集成电路的开发周期，降低开发成本，帮助制造商实现收入最大化。
【学位授予单位】：中国科学院研究生院（计算技术研究所）
【学位级别】：博士
【学位授予年份】：2004
【分类号】：TP332.2

【引证文献】