Equivalence Verification of Large Galois Field Arithmetic Circuits using Word-Level Abstraction via Grobner Bases

Custom arithmetic circuits designed over Galois fields F-2k are prevalent in cryptography, where the field size k is very large (e.g. k = 571-bits). Equivalence checking of such large custom arithmetic circuits against baseline golden models is beyond the capabilities of contemporary techniques. This paper addresses the problem by deriving word-level canonical polynomial representations from gate-level circuits as Z = F (A) over F-2k, where Z and A represent the output and input bit-vectors of the circuit, respectively. Using algebraic geometry, we show that the canonical polynomial abstraction can be derived by computing a Grobner basis of a set of polynomials extracted from the circuit, using a specific elimination (abstraction) term order. By efficiently applying these concepts, we can derive the canonical abstraction in hierarchically designed, custom arithmetic circuits with up to 571-bit datapath, whereas contemporary techniques can verify only up to 163-bit circuits.