As the complexity of digital designs continuously increases, existing methods to ensure their correctness are facing more serious challenges. Although many studies have been provided to enhance the efficiency of debugging methods, they are still suffering from the lack of scalable automatic correction mechanisms. In this paper, we propose a method for correcting multiple design bugs in gate level circuits. To reduce the correction time, an incremental satisfiability-based mechanism is proposed which not only does not require a complete set of test patterns to produce a gate level implementation which does not exhibit erroneous behavior, but also will not reintroduce old bugs after fixing new bugs. The results show that our method can quickly and accurately suggest corrected gates even for large industrial circuits with many bugs. Average improvements in terms of the runtime and memory usage in comparison with existing methods are 2.8× and 6.5×, respectively. Also, the results show that our method compared to the state-of-the-art methods needs 2.6× less test patterns.

The increasing demand for lower power forces designers to use sophisticated power management strategies such as multivoltage and power gating which are often accompanied with many design bugs. Correcting such bugs can be a time-consuming process that requires considerable manual efforts. In this paper, we propose a scalable automated method for correcting dynamic power management architectures by an incremental SAT-based mechanism. First, an initial counterexample (CEX) is generated by checking the equivalency between the specification model of the processor and its buggy implementation model. Then, we find two candidate solutions instead of one to satisfy this CEX. If two solutions are not equivalent, we generate new CEX in an iterative process which effectively converges into the final solution. The proposed method enables designers to correct multiple bugs such as missing isolation cells between two power domains, disordering in the sequence of control signals, error in the data restoring or saving, and powering off in always-on domains which are not addressed by existing methods. We have shown the effectiveness of our method on modern processors supporting complex power management mechanisms. The results confirm that our proposed method, respectively, reduces symbolic simulation steps and runtime by 2.33× and 47.93× compared to the state-of-the-art methods.

Ensuring from the correctness of system on a chip (SoC) designs after the insertion of high level power management strategies that are disconnected from low level controlling signals, is a serious challenge to be addressed. This paper proposes a methodology for formally verifying dynamic power management strategies on implementations in modern processors. The proposed methodology is based on correspondence checking between a golden model without power features as a specification and a pipelined implementation with various power management strategies. Our main contributions in this paper are: 1) extracting Power Management Unit (PMU) from Unified Power Format (UPF) and Global Power Management (GPM), 2) automatically integrating PMU into the implementation and 3) checking the correspondence between two models with efficient symbolic simulation. The experimental results show that our method enables the designers to verify the designs with different power management strategies up to several thousands of lines of Register Transfer Level (RTL) code in minutes. In comparison with existing methods such as [7], our method reduces the number of state variables, the number of clauses, the number of symbolic simulation steps, and the CPU time by 11.04×, 17.57×, 2.08× and 13.71×, respectively.