Arithmetic Circuit Verification Based on Symbolic Computer Algebra
Arithmetic Circuit Verification Based on Symbolic Computer Algebra
复制标题
DOI：
10.1093/ietfec/e91-a.10.3038
复制
发表时间：
2008-10
期刊：
影响因子：
--
通讯作者：
Yuki Watanabe;N. Homma;T. Aoki;T. Higuchi
中科院分区：
文献类型：
--
作者：
Yuki Watanabe;N. Homma;T. Aoki;T. Higuchi
本文提出了一种用符号计算机代数验证算术电路的形式化方法。我们的方法直接描述算术电路与高层次的数学对象的基础上加权数系统和算术公式。这种电路描述可以有效地验证多项式约简技术，使用Grobner基地。本文描述了如何用符号计算机代数来描述和验证算术电路。通过乘累加器和FIR滤波器等运算电路的实验验证，证明了该方法的优越性。结果表明，该方法对实际运算电路的验证具有一定的可行性。
This paper presents a formal approach to verify arithmetic circuits using symbolic computer algebra. Our method describes arithmetic circuits directly with high-level mathematical objects based on weighted number systems and arithmetic formulae. Such circuit description can be effectively verified by polynomial reduction techniques using Grobner Bases. In this paper, we describe how the symbolic computer algebra can be used to describe and verify arithmetic circuits. The advantageous effects of the proposed approach are demonstrated through experimental verification of some arithmetic circuits such as multiply-accumulator and FIR filter. The result shows that the proposed approach has a definite possibility of verifying practical arithmetic circuits.