Formal verification of sequential Galois field arithmetic circuits using algebraic geometry

Sequential Galois field (F_2k) arithmetic circuits take k-bit inputs and produce a k-bit result, after k-clock cycles of operation. Formal verification of sequential arithmetic circuits with large datapath size is beyond the capabilities of contemporary verification techniques. To address this problem, this paper describes a verification method based on algebraic geometry that: (i) implicitly unrolls the sequential arithmetic circuit over multiple (k) clock-cycles; and (ii) represents the function computed by the state-registers of the circuit, canonically, as a multi-variate word-level polynomial over F_2k. Our approach employs the Gröbner basis theory over a specific elimination ideal. Moreover, an efficient implementation is described to identify the k-cycle computation performed by the circuit at word-level. We can verify up to 100-bit sequential Galois field multipliers, whereas conventional techniques fail beyond 23-bit circuits.