Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2m)
Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2m)
复制标题
伽罗瓦域上算术算法的高效验证 GF(2m)
DOI：
10.1007/3-540-44585-4_45
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
T. Yamane
中科院分区：
文献类型：
--
作者：
S. Morioka;Y. Katayama;T. Yamane
伽罗瓦域是GF（2 m）的重要的数制，其广泛用于诸如纠错码（ECC）的应用中，并且在这些应用中执行算术运算的复杂组合。然而，很少有实用的形式化方法，算法验证在字的水平已经开发。我们定义了一个能处理非线性和非凸GF ~（2 m）约束的逻辑系统GF ~（2 m）-算术，用来描述GF（2 m）上算术算法的规范和实现。我们研究了各种判定GF ~（2 m）算法及其子类，并对一个（n，n ~ 4）Reed-Solomon ECC译码算法进行了自动正确性证明。由于正确性准则是在GF（2 m-算术K-域大小无关）的有效子类中，通过使用GF（2 m）上的多项式除法和变量消去的组合，证明在显著减少的时间内完成，对于任何和，m≥ 3和n ≥ 5，不到一秒，而不使用任何昂贵的技术，如因子分解或GF（2）上的决策，这很容易将验证时间增加到一天以上。
The Galois field is an important number system that isGF(2m) widely used in applications such as error correction codes (ECC), and complicated combinations of arithmetic operations are performed in those applications. However, few practical formal methods for algorithm verification at the word-level have ever been developed. We have defined a logic system,GF2m-arithmetic, that can treat non-linear and non-convex GF2m constraints, for describing specifications and implementations of arithmetic algorithms overGF(2m). We have investigated various decisionGF2m-arithmetic and its subclasses, and have performed an automatic correctness proof of a (n, n4) Reed-Solomon ECC decoding algorithm. Because the correctness criterion is in an efficient subclass of theGF2m-arithmeticK-field-size independent), the proof is completed in significantly reduced time, less than one second for any and ,m≥ 3 andn≥ 5, by using a combination of polynomial division and variable elimination overGF(2m), without using any costly techniques such as factoring or a decision overGF(2)that can easily increase the verification time to more than a day.