Rectification of Integer Arithmetic Circuits using Computer Algebra Techniques

This paper proposes a symbolic algebra approach for multi-target rectification of integer arithmetic circuits. The circuit is represented as a system of polynomials and rectified against a polynomial specification with computations modeled over the field of rationals. Given a set of nets as potential rectification targets, we formulate a check to ascertain the existence of rectification functions at these targets. Upon confirmation, we compute the patch functions collectively for the targets. In this regard, we show how to synthesize a logic subcircuit from polynomial artifacts generated over the field of rationals. We present new mathematical contributions and results to substantiate this synthesis process. We present two approaches for patch function computation: a greedy approach that resolves the rectification functions for the targets and an approach that explores a subset of don't care conditions for the targets. Our approach is implemented as custom software and utilizes the existing open-source symbolic algebra libraries for computations. We present experimental results of our approach on several integer multipliers benchmark and discuss the quality of the patch sub-circuits generated.