Method for preparing for and formally verifying a modified integrated circuit design

A method comprising:

• providing a reference integrated circuit (IC) design version including a reference logic block having control logic and datapath logic;
• creating a plurality of modified IC design versions, each including a modified logic block that corresponds to the reference logic block and that includes one or more modifications relative to the reference logic block, wherein the one or more modifications increase in computational complexity from one version to a next version;
• decomposing the reference logic block and each of the modified logic blocks into a datapath logic block and a control logic block;
• and
• performing by a processor, verifying sequential equivalence of logic between each modified IC design version and a next modified IC design version having a greater modification computational complexity, beginning with the reference IC design version and a first modified IC design version having a least modification computational complexity;
• wherein verifying sequential equivalence of logic between each modified IC design version and a next modified IC design version having a greater modification computational complexity includes instantiating a given modified IC design version and performing additional modifications to create a corresponding next modified IC design, and verifying sequential equivalence of logic between the given modified IC design version and the corresponding next modified IC design.

A non-transitory computer readable storage medium including program instructions for preparing an integrated circuit (IC) design for formal sequential equivalence checking, the program instructions are executable by a processor to:

• provide a reference integrated circuit (IC) design version including a reference logic block having datapath logic and control logic;
• create a plurality of modified IC design versions, each including a modified logic block that corresponds to the reference logic block and that includes one or more modifications relative to the reference logic block, wherein the one or more modifications increase in computational complexity from one version to a next version;
• receiving information that corresponds to a decomposition of the reference logic block and each of the modified logic blocks into a datapath logic block and a control logic block;
• and
• verify sequential equivalence of logic between each IC design version and a next IC design version having a greater modification computational complexity, beginning with the reference IC design version and a first modified IC design version having a least modification computational complexity;
• wherein the program instructions are further executable by the processor to instantiate a given modified IC design version and perform additional modifications to create a corresponding next modified IC design, and verify sequential equivalence of logic between the given modified IC design version and the corresponding next modified IC design.

A system comprising:

• a memory storing program instructions for preparing an integrated circuit (IC) design for formal sequential equivalence checking;
• a processor coupled to the memory, wherein the processor, in response to executing the instructions is configured to:
• provide a reference integrated circuit (IC) design version including a reference logic block having datapath logic and control logic;
• create a plurality of modified IC design versions, each including a modified logic block that corresponds to the reference logic block and that includes one or more modifications relative to the reference logic block, wherein the one or more modifications increase in computational complexity from one version to a next version;
• decompose the reference logic block and each of the modified logic blocks into a datapath logic block and a control logic block;
• and
• verify sequential equivalence of logic between each IC design version and a next IC design version having a greater modification computational complexity, beginning with the reference IC design version and a first modified IC design version having a least modification computational complexity;
• wherein the modified logic block within each IC design version is at a same level of hierarchy as the modified logic block in the next modified IC design version.

A method comprising:

• providing a reference integrated circuit (IC) design version including a reference logic block;
• separating a datapath logic and a control logic within the reference logic block;
• encapsulating the datapath logic within a module that has a different level of hierarchy than the control logic within the reference IC design version;
• creating a plurality of modified IC design versions from the reference IC design, wherein each modified IC design version includes a modified logic block that corresponds to the reference logic block and that includes one or more modifications relative to the reference logic block, wherein the one or more modifications increase in computational complexity from one version to a next version;
• performing by a processor, verifying sequential equivalence of logic between the reference IC design version and a first modified IC design version having a least modification computational complexity;
• iteratively verifying sequential equivalence of logic between each modified IC design version and a next modified IC design version having a greater modification computational complexity;
• wherein the modified logic block within each IC design version is at a same level of hierarchy as the modified logic block in the next modified IC design version.