Using traces of original model to verify a modified model

A computerized apparatus having a processor, the processor being adapted to perform the steps of:

• obtaining a trace exemplifying a checker failing in a model;
• obtaining a modified model, wherein the modified model is a modified version of the model which was modified in an attempt to resolve the checker failing in the model;
• re-simulating the trace in the modified model to generate a second trace, wherein said re-simulating is performed by a processor;
• comparing the trace and the second trace to identify a common prefix, wherein the common prefix ends immediately before a cycle in which a state according to the trace is different than a state according to the second trace;
• and
• guiding verification of the modified model using values derived from the common prefix.

A computer program product comprising:

• a non-transitory computer readable medium retaining program instructions, which instructions when read by a processor, case the processor to performs the steps of:
• obtaining a trace exemplifying a checker failing in a model;
• obtaining a modified model, wherein the modified model is a modified version of the model which was modified in an attempt to resolve the checker failing in the model;
• re-simulating the trace in the modified model to generate a second trace, wherein said re-simulating is performed by a processor;
• comparing the trace and the second trace to identify a common prefix, wherein the common prefix ends immediately before a cycle in which a state according to the trace is different than a state according to the second trace;
• and
• guiding verification of the modified model using values derived from the common prefix.