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