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

吉林大学学报(工学版) ›› 2009, Vol. 39 ›› Issue (05): 1309-1313.

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

吴俊华^1,2,李东海¹,马光胜¹,李光顺²

1.哈尔滨工程大学计算机科学与技术学院,哈尔滨 150001；2.曲阜师范大学计算机科学学院,山东日照 276826

收稿日期:2008-03-14 出版日期:2009-09-01 发布日期:2009-09-01
通讯作者: 马光胜（1944-）,男,教授,博士生导师.研究方向:EDA理论与算法.Email:maguangsheng@hrbeu.edu.cn E-mail:maguangsheng@hrbeu.edu.cn
作者简介:吴俊华（1979-）,女,博士研究生.研究方向:EDA设计方法.Email:shdwjh@163.com
基金资助:
国家自然科学基金项目（60273081）.

Simulation based equivalence verification for fixedpoint arithmetic datapaths

WU Jun-hua^1,2, LI Dong-hai¹, MA Guang-sheng¹,LI Guang-shun²

1.College of Computer Science and Technology, Harbin Engineering University, Harbin 150001, China|2.College of Computer Science, Qufu Normal University, Rizhao 276826

Received:2008-03-14 Online:2009-09-01 Published:2009-09-01

摘要/Abstract

摘要：

为证明定点数据通路的定点算术规范与转换后的寄存器传输级实现是等价的，结合算术转换和多项式函数对实现序列加法、乘法、移位运算的定点数据通路进行建模，根据多项式函数的结论得到对定点数据通路进行等价验证所需要的模拟向量数的上界，避免穷举所有的模拟向量。实验结果证明本文提出的方法是有效的。

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

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 the proposed method is effective.

Key words: computersystemarchitecture, equivalence verification, datapaths, polynomialfunction, arithmetictransforms

中图分类号:

TP302.1

吴俊华, 李东海, 马光胜, 李光顺. 基于模拟的定点算术数据通路等价性验证[J]. 吉林大学学报(工学版), 2009, 39(05): 1309-1313.

WU Jun-Hua, LI Dong-Hai, MA Guang-Sheng, LI Guang-Shun. Simulation based equivalence verification for fixedpoint arithmetic datapaths[J]. 吉林大学学报(工学版), 2009, 39(05): 1309-1313.

参考文献

相关文章 15

[1]	余宜诚, 胡亮, 迟令, 初剑峰. 一种改进的适用于多服务器架构的匿名认证协议[J]. 吉林大学学报(工学版), 2018, 48(5): 1586-1592.
[2]	董坚峰, 张玉峰, 戴志强. 改进的基于狄利克雷混合模型的推荐算法[J]. 吉林大学学报(工学版), 2018, 48(2): 596-604.
[3]	赵博, 秦贵和, 赵永哲, 杨文迪. 基于半陷门单向函数的公钥密码[J]. 吉林大学学报(工学版), 2018, 48(1): 259-267.
[4]	刘磊, 刘利娟, 吴新维, 张鹏. 基于ECPMR的编译器测试方法[J]. 吉林大学学报(工学版), 2017, 47(4): 1262-1267.
[5]	董立岩, 王越群, 贺嘉楠, 孙铭会, 李永丽. 基于时间衰减的协同过滤推荐算法[J]. 吉林大学学报(工学版), 2017, 47(4): 1268-1272.
[6]	于斌斌, 武欣雨, 初剑峰, 胡亮. 基于群密钥协商的无线传感器网络签名协议[J]. 吉林大学学报(工学版), 2017, 47(3): 924-929.
[7]	邓昌义, 郭锐锋, 张忆文, 王鸿亮. 基于平衡因子的动态偶发任务低功耗调度算法[J]. 吉林大学学报(工学版), 2017, 47(2): 591-600.
[8]	魏晓辉, 刘智亮, 庄园, 李洪亮, 李翔. 支持大规模流数据在线处理的自适应检查点机制[J]. 吉林大学学报(工学版), 2017, 47(1): 199-207.
[9]	郝娉婷, 胡亮, 姜婧妍, 车喜龙. 基于多管理节点的乐观锁协议[J]. 吉林大学学报(工学版), 2017, 47(1): 227-234.
[10]	魏晓辉, 李翔, 李洪亮, 李聪, 庄园, 于洪梅. 支持大规模流数据处理的弹性在线MapReduce模型及拓扑协议[J]. 吉林大学学报(工学版), 2016, 46(4): 1222-1231.
[11]	车翔玖, 梁森. 一种基于大顶堆的SPIHT改进算法[J]. 吉林大学学报(工学版), 2016, 46(3): 865-869.
[12]	董悦丽, 郭权, 孙斌, 康玲. 药物分子对接动态任务迁移优化[J]. 吉林大学学报(工学版), 2015, 45(4): 1253-1259.
[13]	匡哲君，师唯佳，胡亮. 基于无线传感器网络的角色成员关系剩余能量新算法[J]. 吉林大学学报(工学版), 2015, 45(2): 600-605.
[14]	张忆文，郭锐锋. 实时系统混合任务低功耗调度算法[J]. 吉林大学学报(工学版), 2015, 45(1): 261-266.
[15]	张忆文^{1, 2}, 郭锐锋¹. 制的容错节能调度算法[J]. 吉林大学学报(工学版), 2014, 44(4): 1112-1117.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed