基于模拟的定点算术数据通路等价性验证  

Simulation-based equivalence verification for fixed-point arithmetic datapaths

作　　者：吴俊华[1,2] 李东海[1] 马光胜[1] 李光顺[2] 

机构地区：[1]哈尔滨工程大学计算机科学与技术学院,哈尔滨150001 [2]曲阜师范大学计算机科学学院,山东日照276826

出　　处：《吉林大学学报（工学版）》2009年第5期1309-1313,共5页Journal of Jilin University:Engineering and Technology Edition

基　　金：国家自然科学基金项目(60273081)

摘　　要：为证明定点数据通路的定点算术规范与转换后的寄存器传输级实现是等价的,结合算术转换和多项式函数对实现序列加法、乘法、移位运算的定点数据通路进行建模,根据多项式函数的结论得到对定点数据通路进行等价验证所需要的模拟向量数的上界,避免穷举所有的模拟向量。实验结果证明本文提出的方法是有效的。In order to prove that the fixed-point arithmetic specification is equivalence to the translated Register Transfer Level （RTL） implementation, the fixed-point datapaths, which perform ADD, MULT and SHIFT operations, are modeled by combining arithmetic transform （AT） and polynomial function. According to the results of polynomial function, the upper bound of simulated vectors is obtained for the equivalence verification of the fixed-point datapaths, which avoids the exhaustive simulation. Experiment results show that the proposed method is effective.

关 键 词：计算机系统结构 等价验证 数据通路 多项式函数 算术转换 

分 类 号：TP302.1[自动化与计算机技术—计算机系统结构]