In this paper we discuss techniques by which C descriptions corresponding to given implementation designs can be automatically reproduced. Once they are generated, they are compared with the original C designs to make sure that the implementation designs are correct, i.e., they are equivalent to the original C designs. In the cases where ECO (Engineering Change Order) is applied to the implementation designs, the generated C descriptions from them represent the behaviors of the implementation designs after ECO, and by comparing them with the original C designs, the actual behavioral difference, if any (some ECO, such as timing ECO, may not change the behaviors), between the two can be understood in C language level, which should be very informative for designers. In the proposed method, templates are generated from the original C descriptions by replacing a set of statements with parametrized and programmable statements having symbolic variables and constants that represent program variables, constants, operators and others. Then the problem to refine the templates so that the resulting C descriptions become equivalent to the implementation designs is formulated as QBF (Quantified Boolean Formula) problems. The QBF problems are solved by repeatedly applying SAT solvers in incremental ways without any formal analysis on the implementation designs. The proposed method relies only on simulations of implementation designs and never formally analyzes them, i.e., implementation designs are just simulated by a number of times (ten times to one hundred times or so in the experiments). and the generated C descriptions are 100\% equivalent to the implementation designs as long as templates are right ones. We show preliminary experimental results which show usefulness of the proposed approach.