Master of Science

thesisFormal verification of arithmetic circuits checks whether or not a gate-level circuit correctly implements a given specification model. In recent years, verification of arithmetic circuits has received a lot of attention. However, rectification of arithmetic circuits has only been addressed very recently. This is an important problem that finds application not only in debugging, but also in engineering change orders and synthesis of approximate circuits. This master's thesis addresses the problem of rectification of integer arithmetic circuits using concepts from symbolic computer algebra. When formal verification identifies the presence of a bug in the design, rectification needs to be performed to correct the function implemented by the circuit, so that it matches the given specification. Using concepts from symbolic computer algebra and algebraic geometry, we identify a net in the circuit such that, irrespective of the number or type of bugs/errors, the circuit can be rectified at that one particular net. This is called single-fix rectification. Once single-fix rectifiability of the circuit is ascertained, we compute a corresponding rectification function at the target net which corrects the circuit. The algorithmic approaches are based on the Gr¨obner basis algorithm, which is used as both a decision procedure (for ascertaining rectifiability) as well as a quantification procedure (for computing a rectification function). While this problem has been recently solved for finite field arithmetic circuits, this thesis investigates the application to integer arithmetic circuits, while presenting new theory, techniques, and algorithmic implementations to rectify integer multiplier circuits