| 基于模拟的定点算术数据通路等价性验证 |
| |
| 引用本文： | 吴俊华,李东海,马光胜,李光顺.基于模拟的定点算术数据通路等价性验证[J].吉林大学学报(工学版),2009,39(5). |
| |
| 作者姓名： | 吴俊华 李东海 马光胜 李光顺 |
| |
| 作者单位： | 1. 哈尔滨工程大学计算机科学与技术学院,哈尔滨,150001;曲阜师范大学计算机科学学院,山东,日照,276826
2. 哈尔滨工程大学计算机科学与技术学院,哈尔滨,150001 |
| |
| 基金项目： | 国家自然科学基金项目(60273081) |
| |
| 摘 要： | 为证明定点数据通路的定点算术规范与转换后的寄存器传输级实现是等价的,结合算术转换和多项式函数对实现序列加法、乘法、移位运算的定点数据通路进行建模,根据多项式函数的结论得到对定点数据通路进行等价验证所需要的模拟向量数的上界,避免穷举所有的模拟向量。实验结果证明本文提出的方法是有效的。
|
| 关 键 词： | 计算机系统结构 等价验证 数据通路 多项式函数 算术转换 |
Simulation-based equivalence verification for fixed-point arithmetic datapaths |
| |
| WU Jun-hua,LI Dong-hai,MA Guang-sheng,LI Guang-shun.Simulation-based equivalence verification for fixed-point arithmetic datapaths[J].Journal of Jilin University:Eng and Technol Ed,2009,39(5). |
| |
| Authors: | WU Jun-hua LI Dong-hai MA Guang-sheng LI Guang-shun |
| |
| Affiliation: | 1.College of Computer Science and Technology;Harbin Engineering University;Harbin 150001;China;2.College of Computer Science;Qufu Normal University;Rizhao 276826 |
| |
| Abstract: | 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 ... |
| |
| Keywords: | computer system architecture equivalence verification datapaths polynomial function arithmetic transforms |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
