| 基于多项式符号代数方法的高层次数据通路的等价验证 |
| |
| 引用本文： | 杨志,马光胜,张曙.基于多项式符号代数方法的高层次数据通路的等价验证[J].计算机研究与发展,2009,46(3). |
| |
| 作者姓名： | 杨志 马光胜 张曙 |
| |
| 作者单位： | 1. 哈尔滨工程大学计算机科学与技术学院,哈尔滨,150001
2. 哈尔滨工程大学信息与通信工程学院,哈尔滨,150001 |
| |
| 摘 要： | 基于BDD或布尔SAT的等价验证方法虽然能够成功验证低层次门级电路,但却难以满足高层次设计验证要求.由此,以多项式符号代数为理论基础,提出了一个高层次数据通路的等价验证算法.深入研究了使用多项式表达式描述复杂数据通路行为的方法,得到了高层次数据通路的多项式集合表示的一般形式.从多项式集合公共零点的角度定义了高层次数据通路的功能等价,给出了一个基于Gr(o)bner基计算的有效代数求解算法.针对不同基准数据通路的实验结果表明了该算法的有效性.
|
| 关 键 词： | 高层次数据通路 等价验证 多项式符号代数 形式验证 电子设计自动化 |
Equivalence Verification of High-Level Datapaths Based on Polynomial Symbolic Algebra |
| |
| Yang Zhi,Ma Guangsheng,Zhang Shu.Equivalence Verification of High-Level Datapaths Based on Polynomial Symbolic Algebra[J].Journal of Computer Research and Development,2009,46(3). |
| |
| Authors: | Yang Zhi Ma Guangsheng Zhang Shu |
| |
| Affiliation: | College of Computer Science and Technology;Harbin Engineering University;Harbin 150001;College of Information and Communication Engineering;Harbin 150001 |
| |
| Abstract: | As the size and functional complexity of IC designs increase,it has become important to address verification issues at early stages of the IC design flow.This means that IC designers require automated verification tools at higher levels of abstraction.Because of this,formal verification methods,such as equivalence verification,have become important for register transfer level or behavioral level verification.However,most of the existing techniques for equivalence verification are based on BDD or Boolean SAT... |
| |
| Keywords: | high-level datapaths equivalence verification polynomial symbolic algebra formal verification electronic design automation |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
