...
首页> 外文期刊>IEEE Transactions on Computers >Formal Approach for Verifying Galois Field Arithmetic Circuits of Higher Degrees
【24h】

Formal Approach for Verifying Galois Field Arithmetic Circuits of Higher Degrees

机译:验证高次Galois场算术电路的形式化方法

获取原文
获取原文并翻译 | 示例
           

摘要

This paper presents an efficient approach to verifying higher-degree Galois-field (GF) arithmetic circuits. The proposed method describes GF arithmetic circuits using a mathematical graph-based representation and verifies them by a combination of algebraic transformations and a new verification method based on natural deduction for first-order predicate logic with equal sign. The natural deduction method can verify one type of higher-degree GF arithmetic circuit efficiently while the existing methods require an enormous amount of time, if they can verify them at all. In this paper, we first apply the proposed method to the design and verification of various Reed-Solomon (RS) code decoders. We confirm that the proposed method can verify RS decoders with higher-degree functions while the existing method needs a lot of time or fail. In particular, we show that the proposed method can be applied to practical decoders with 8-bit symbols, which are performed with up to 2,040-bit operands. We then demonstrate the design and verification of the Advanced Encryption Standard (AES) encryption and decryption processors. As a result, the proposed method successfully verifies the AES decryption datapath while an existing method fails.
机译:本文提出了一种验证高次Galois场(GF)算术电路的有效方法。所提出的方法使用基于数学图的表示来描述GF算术电路,并通过代数变换与基于自然演绎的等号一阶谓词逻辑的新验证方法相结合来对其进行验证。自然推论方法可以有效地验证一种类型的高阶GF运算电路,而现有方法则需要大量时间才能验证它们。在本文中,我们首先将提出的方法应用于各种Reed-Solomon(RS)码解码器的设计和验证。我们确认,该方法可以验证具有较高功能的RS解码器,而现有方法则需要大量时间或失败。特别地,我们表明,所提出的方法可以应用于具有8位符号的实际解码器,该解码器最多可以使用2,040位操作数执行。然后,我们演示高级加密标准(AES)加密和解密处理器的设计和验证。结果,所提出的方法成功地验证了AES解密数据路径,而现有方法却失败了。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号