Methods of Equivalence Checking and ECO Support under C-based Design through Reproduction of C Descriptions from Implementation Designs

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 is applied, which should be very informative for designers. We use template-based approach where the original C descriptions are expanded to have parametrized descriptions. Parameters include program variables, symbolic constants, and programmable statements and define sets of possible behaviors by the C descriptions. If we can refine the templates so that the resulting C descriptions become equivalent to the implementation designs, the appropriate C descriptions corresponding to the implementations after ECO is generated. This refinement problem can be formulated as QBF (Quantified Boolean Formula) problems which are solved by repeatedly applying SAT solvers in incremental ways without any formal analysis on the implementation designs. It is noted that the implementation designs are never formally analyzed. The implementation designs just need to be simulated for some concrete input values by ten times to one hundred times or so in our experiments.