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.

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.

In this paper we propose a new timing verification technique named coded time-symbolic simulation, CTSS. Our interest is on simulation of logic circuits consisting of gates whose delay is specified only by its minimum and maximum values. Conventional logic simulation based on min/max delay model leads to over-pessimistic results. In our new method, the cases of possible delay values of each gate are encoded by binary vectors. The circuit behavior for all the possible combinations of the delay values are simulated based on symbolic simulation by assigning Boolean variables to the binary vectors. This simulation technique can deal with logic circuits containing feedback loops as well as combinational circuits. We implemented an efficient simulator by using shared binary decision diagrams (SBDD's) as internal representation of Boolean functions. We also propose novel techniques of analyzing the results of CTSS.