Formal Verification of Constrained Arithmetic Circuits using Computer Algebraic Approach

This paper presents a novel verification method for arithmetic circuits subjected to some user or application constraints. The verification problem is solved in an algebraic domain rather than in a Boolean domain by representing circuit specification and its implementation as polynomials. The concept of deterministic terms is introduced to describe the constraints imposed on the circuit. Based on this concept, a case splitting analysis is proposed to resolve the memory problem during algebraic rewriting. The computational complexity of the method is analyzed, and two techniques are proposed to accelerate the verification process. The experimental results for constrained arithmetic circuits up to 128 bits, and the comparison with the state-of-the-art SAT solver demonstrate the effectiveness and the scalability of the proposed method.