Automated Design Debugging With Maximum Satisfiability

As contemporary VLSI designs grow in complexity, design debugging has rapidly established itself as one of the largest bottlenecks in the design cycle today. Automated debug solutions such as those based on Boolean Satisfiability (SAT) enable engineers to reduce the debug effort by localizing possible error sources in the design. Unfortunately, adaptation of these techniques to industrial designs is still limited by the performance and capacity of the underlying engines. This paper presents a novel formulation of the debugging problem using MaxSat to improve the performance and applicability of automated debuggers. Our technique not only identifies errors in the design but also indicates when the bug is excited in the error trace. MaxSat allows for a simpler formulation of the debugging problem, reducing the problem size by 80% compared to a conventional SATbased technique. Empirical results demonstrate the effectiveness of the proposed formulation as run-time improvements of 4.5

• Type: Journal
• Year: 2010
• Where: TCAD
• Authors: Yibin Chen, Sean Safarpour, João Marques-Silva, Andreas G. Veneris
• Keywords: Debugging Problem, Design, Error Sources, Software Engineering, TCAD 2010