Bijan Alizadeh
University of Tehran
Fault 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 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.