Efficient Symbolic Computation for Word-Level Abstraction From Combinational Circuits for Verification Over Finite Fields

This paper introduces a technique to derive a word-level abstraction of the function implemented by a combinational logic circuit. The abstraction provides a canonical representation of the function as a polynomial <tex-math notation="LaTeX">Z = F(A) </tex-math> over the finite field <tex-math notation="LaTeX">F_2ᵏ </tex-math> , where <tex-math notation="LaTeX">Z </tex-math> and <tex-math notation="LaTeX">A </tex-math> represent the <tex-math notation="LaTeX">k </tex-math> -bit output and input bit-vectors (words) of the circuit, respectively. This canonical abstraction can be utilized for formal verification and equivalence checking of combinational circuits. Our approach to abstraction is based upon concepts from computational commutative algebra and algebraic geometry. We show that the abstraction <tex-math notation="LaTeX">Z = F(A) </tex-math> can be derived by computing a Gröbner basis of the polynomials corresponding to the circuit, using a specific elimination term order derived from the circuit’s topology. Computing Gröbner bases using elimination term orders is infeasible for large circuits. To overcome this limitation, we describe an efficient symbolic computation to derive the word-level polynomial. Our algorithms exploit: 1) the structure of the circuit; 2) the properties of Gröbner bases; 3) characteristics of finite fields <tex-math notation="LaTeX">F_2ᵏ </tex-math> ; and 4) modern algorithms from symbolic algebra, to derive the canonical polynomial representation. This approach is employed to verify (and detect bugs in) large combinational finite field arithmetic circuits, where contemporary verification techniques are known to be infeasible.