Method and system for sequential equivalence checking

A system for sequential equivalence checking (SEC) of two non-abstracted representations of an electronic design, the system comprising:

• a memory;
• and
• a processor configured to:
• select a plurality of cutpoints in the two non-abstracted representations of the electronic design, rendering the two non-abstracted representations of the electronic design abstracted;
• execute an assume-guarantee (AG) proof on the two abstracted representations of the electronic design;
• identify a failed assertion indicating non-equivalence of a signal pair relating to one of the cutpoints;
• discard said plurality of cutpoints from the two abstracted representations of the electronic design;
• and
• perform a simulation on the two non-abstracted representations of the electronic design by successively inputting input stimuli of a trace corresponding to the failed assertion in a sequential order in which the input stimuli appear in the trace at inputs of the two non-abstracted representations of the electronic design to identify whether there is one or a plurality of additional non-equivalent signal pairs relating to other cutpoints of said plurality of cutpoints.

A non-transitory computer readable storage medium for sequential equivalence checking of two non-abstracted representations of an electronic design, having stored thereon instructions that when executed by a processor will cause the processor to:

• select a plurality of cutpoints in the two non-abstracted representations of the electronic design, rendering the two non-abstracted representations of the electronic design abstracted;
• execute an assume-guarantee (AG) proof on the two abstracted representations of the electronic design;
• identify a failed assertion indicating non-equivalence of a signal pair relating to one of the cutpoints;
• and
• perform a simulation on the two non-abstracted representations of the electronic design by successively inputting input stimuli of a trace corresponding to the failed assertion in a sequential order in which the input stimuli appear in the trace at inputs of the two non-abstracted representations of the electronic design to identify whether there is one or a plurality of additional non-equivalent signal pairs relating to other cutpoints of said plurality of cutpoints.