As integrated circuits scale up, localizing errors during silicon debug becomes very challenging and time-consuming. To free human-beings from this tedious work, my work focus on detecting and localizing bugs by using the automatic formal techniques. More specifically, a hardware design or a software test can be transformed into a symbolic math representation, such that a modern decision procedure tool, e.g. Satisfiability (SAT) or Satisfiability Modular Theory (SMT) solver, can further analyze the verification problem. As an application of artificial intelligence, such decision-making and theorem-proving techniques can facilitate the hardware debugging process without human engagement. However, the main challenge of this approach comes from the scalability limitation of the decision procedure, especially when it is applied to a huge circuit or a concurrent software test. In this project, we try to address the possible solutions from this point of view.