An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths
An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths
复制标题
证明算术数据路径中数据正确性的代数方法
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
G. Greuel
中科院分区：
文献类型：
--
作者：
Oliver Wienand;Markus Wedler;D. Stoffel;W. Kunz;G. Greuel
提出了一种新的验证片上系统模块中数据通路算法正确性的方法。它是对现有技术的补充，由于复杂性的原因，这些技术仅限于验证控制行为。该电路是在算术位级(ABL)上建模的，因此我们的方法很好地适应了当前高性能数据路径的工业设计风格。ABL的正规化与计算机代数的技术相结合。我们计算了环上的Grobner基的标准形。事实证明，我们的方法对于标准属性检查技术失败的工业数据路径设计是容易处理的。
This paper proposes a new approach for proving arithmetic correctness of data paths in System-on-Chip modules. It complements existing techniques which are, for reasons of complexity, restricted to verifying only the control behavior. The circuit is modeled at the arithmetic bit level (ABL) so that our approach is well adapted to current industrial design styles for high performance data paths. Normalization at the ABL is combined with the techniques of computer algebra. We compute normal forms with respect to Grobner bases over rings i¾?/$\left\langle{2^n}\right\rangle$. Our approach proves tractable for industrial data path designs where standard property checking techniques fail.