Post-silicon debugging is getting even more critical to shorten the time-to-market than ever, as many more bugs escape pre-silicon verification according to the increasing design scale and complexity. Post-silicon debugging is generally harder than pre-silicon debugging due to the limited observability and controllability of internal signal values. Conventionally, simulation of corresponding low-level designs such as RTL or gate-level has been used to get observability and controllability, which is inefficient for contemporary large designs. In this paper, we introduce a post-silicon debugging approach using simulation of high-level designs, instead of low-level designs. To realize such a debugging approach, we propose an I/O sequence mapping method that converts I/O sequences of chip executions to those of the corresponding high-level design. First, we provide a formal definition of I/O sequence mapping and relevant notions. Then, based on the definition, we propose an I/O sequence mapping method by executing FSMs representing the interface specifications of the target design. Also, we propose an implementation of the proposed method to get further efficiency. We demonstrate that the proposed method can be effectively applied to several practical design examples with various interfaces.

Equivalence checking is one of the most important issues in VLSI design to guarantee that bugs do not enter designs during optimization steps or synthesis steps. In this paper, we propose a new word-level equivalence checking method between two models before and after high-level synthesis or behavioral optimization. Our method converts two given designs into RTL models which have same datapaths so that behaviors by identical control signals become the same in the two designs. Also, functional units become common to the two designs. Then word-level equivalence checking techniques can be applied in bit-level accuracy. In addition, we propose a rule-based equivalence checking method which can verify designs which have complicated control structures faster than existing symbolic simulation based methods. Experimental results with realistic examples show that our method can verify such designs in practical periods.

In this paper, an efficient equivalence checking method for two C descriptions is described. The equivalence of two C descriptions is proved by symbolic simulation. Symbolic simulation used in this paper can prove the equivalence of all of the variables in the descriptions. However, it takes long time to verify the equivalence of all of the variables if large descriptions are given. Therefore, in order to improve the verification, our method identifies textual differences between descriptions. The identified textual differences are used to reduce the number of equivalence checkings among variables. The proposed method has been implemented in C language and evaluated with several C descriptions.

Bounded model checking is a widely used formal technique in both hardware and software verification. However, it cannot be applied if the bounds (number of time frames to be analyzed) become large, and deep bugs which are observed only through very long counter-examples cannot be detected. This paper presents a method concatenating multiple bounded model checking results efficiently with symbolic simulation. A bounded model checking with a large bound is recursively decomposed into multiple ones with smaller bounds, and symbolic simulation on each counterexample supports smooth connections to the others. A strong heuristic for the proposed method that targets deep bugs is also presented, and can be applied together with other efficient bounded model checking methods since it does not touch the basic bounded model checking algorithm.