Symbolic model-based diagnosis with auto-correction framework for arithmetic circuits

Design error detection, localization and correction are considered as important and difficult tasks in the arithmetic circuit debugging process. In this paper we present a symbolic model-based diagnosis framework for arithmetic circuit debugging which can deal with modulo equivalence based on a canonical decision diagram called Modular Horner Expansion Diagram (M-HED) in order to verify the equivalence of an and-inverter-graph (AIG) representation as the gate level implementation against a polynomial expression over Z_2n as the specification. If two models are not equivalent, our approach is able to automatically correct the AIG according to the specification. We evaluate our approach on several large arithmetic circuits thereby showing performance benefits of many orders of magnitude than widely accepted industrial techniques.