Formal Approach for Verifying Galois Field Arithmetic Circuits of Higher Degrees

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.