Combining Symbolic Computer Algebra and Boolean Satisfiability for Automatic Debugging and Fixing of Complex Multipliers

If verification of a digital circuit fails, then debugging and fixing become the major subsequent tasks. Arithmetic units are among the most challenging circuits for debugging because of a wide variety of architectures and high design complexity. A prominent example are multipliers. Since existing automatic methods fail for these circuits, both tasks are performed manually which is typically very time-consuming. In this paper, we propose a complete debugging flow based on the combination of Symbolic Computer Algebra (SCA) and Boolean Satisfiability (SAT). Complete means that our method targets the complete loop until the arithmetic circuit is guaranteed to fulfill its specification. For this, our approach consists of the three phases verification, localization, and fixing. In the experimental evaluation, we demonstrate the applicability of our approach for the most complex multiplier architectures.