Latch modeling technique for formal verification

A method for performing formal verification of an integrated circuit (IC) design, the method comprising:

• identifying a set of remodeling-eligible latches in a synthesized layout of sequential logic for the IC design, each of the set of remodeling-eligible latches exhibiting flip flop output behavior;
• replacing each of the set of remodeling-eligible latches in the synthesized layout with a flip flop to form a remodeled layout;
• and
• performing clock modeling on the remodeled layout,
• wherein identifying the set of remodeling-eligible latches comprises:
• applying cone partitioning to the synthesized layout to determine a data fan-in cone and a first clock net for a test latch in the synthesized layout, wherein cone partitioning starts at a latch pin and expands out recursively to compile upstream logic until one of a primary input and a sequential logic gate is reached;
• and
• including the test latch in the set of remodeling-eligible latches if:
• the data fan-in cone does not include a primary input to the synthesized layout;
• the data fan-in cone does not include a first sequential logic gate driven by a second clock net that is not identical to the first clock net;
• and
• the data fan-in cone does not include a second sequential logic gate that exhibits a first phase behavior that is equivalent to a second phase behavior of the test latch.

A method for performing formal verification of an integrated circuit (IC) design, the method comprising:

• identifying a set of remodeling-eligible latches in a synthesized layout of sequential logic for the IC design, each of the set of remodeling-eligible latches exhibiting flip flop output behavior;
• replacing each of the set of remodeling-eligible latches in the synthesized layout with a flip flop to form a remodeled layout;
• and
• performing clock modeling on the remodeled layout,
• wherein identifying the set of remodeling-eligible latches comprises:
• applying cone partitioning to the synthesized layout to determine a data fan-in cone and a clock net for each latch in the synthesized layout, wherein cone partitioning starts at a latch pin and expands out recursively to compile upstream logic until one of a primary input and a sequential logic gate is reached;
• excluding a first set of latches from the set of remodeling-eligible latches, wherein the data fan-in cone of each of the first set of latches includes a primary input to the synthesized layout;
• excluding a second set of latches from the set of remodeling-eligible latches, wherein the data fan-in cone of each of the second set of latches includes at least one sequential logic gate driven by a first clock net, wherein the first clock net is not equivalent to a second clock net driving the each of the second set of latches;
• and
• excluding a third set of latches from the set of remodeling-eligible latches, wherein the data fan-in cone for each of the third set of latches includes a first sequential logic gate having a first phase behavior that is equivalent to a second phase behavior of the each of the third set of latches.

A system for performing formal verification of an integrated circuit (IC) design, the system comprising:

• latch selection logic for identifying a first set of latches in a synthesized layout of the IC design, each of the first set of latches exhibiting flip flop output behavior;
• latch replacement logic for replacing each of the first set of latches in the synthesized layout with a flip flop to generate a remodeled layout;
• and
• clock modeling logic for performing clock modeling on the remodeled layout,
• wherein the latch selection logic comprises:
• logic for applying cone partitioning to the synthesized layout to determine a data fan-in cone and a first clock net for a test latch in the synthesized layout, wherein cone partitioning starts at a latch pin and expands out recursively to compile upstream logic until one of a primary input and a sequential logic gate is reached;
• and
• logic for including the test latch in the set of remodeling-eligible latches if:
• the data fan-in cone does not include a primary input to the synthesized layout;
• the data fan-in cone does not include a first sequential logic gate driven by a second clock net that is not functionally equivalent to the first clock net;
• and
• the data fan-in cone does not include a second sequential logic gate that exhibits a first phase behavior that is equivalent to a second phase behavior of the test latch.

A system for performing formal verification of an integrated circuit (IC) design, the system comprising:

• latch selection logic for identifying a first set of latches in a synthesized layout of the IC design, each of the first set of latches exhibiting flip flop output behavior;
• latch replacement logic for replacing each of the first set of latches in the synthesized layout with a flip flop to generate a remodeled layout;
• and
• clock modeling logic for performing clock modeling on the remodeled layout,
• wherein the latch selection logic comprises:
• logic for applying cone partitioning to the synthesized layout to determine a data fan-in cone and a first clock net for a test latch in the synthesized layout, wherein cone partitioning starts at a latch pin and expands out recursively to compile upstream logic until one of a primary input and a sequential logic gate is reached;
• and
• logic for including the test latch in the set of remodeling-eligible latches if:
• the first data fan-in cone does not include a primary input to the synthesized layout;
• the data fan-in cone does not include a first sequential logic gate driven by a second clock net that is not identical to the first clock net;
• and
• the data fan-in cone does not include a second sequential logic gate that exhibits a first phase behavior that is equivalent to a second phase behavior of the test latch.

A system for performing formal verification of an integrated circuit (IC) design, the system comprising:

• latch selection logic for identifying a first set of latches in a synthesized layout of the IC design, each of the first set of latches exhibiting flip flop output behavior;
• latch replacement logic for replacing each of the first set of latches in the synthesized layout with a flip flop to generate a remodeled layout;
• and
• clock modeling logic for performing clock modeling on the remodeled layout,
• wherein the latch selection logic comprises:
• logic for applying cone partitioning to the synthesized layout to determine a data fan-in cone and a clock net for each latch in the synthesized layout, wherein cone partitioning starts at a latch pin and expands out recursively to compile upstream logic until one of a primary input and a sequential logic gate is reached;
• logic for excluding a first set of latches from the set of remodeling-eligible latches, wherein the data fan-in cone of each of the first set of latches includes a primary input to the synthesized layout;
• logic for excluding a second set of latches from the set of remodeling-eligible latches, wherein the data fan-in cone of each of the second set of latches includes at least one sequential logic gate driven by a first clock net, wherein the first clock net is not equivalent to a second clock net driving the each of the second set of latches;
• and
• logic for excluding a third set of latches from the set of remodeling-eligible latches, wherein the data fan-in cone for each of the third set of latches includes a first sequential logic gate having a first phase behavior that is equivalent to a second phase behavior of the each of the third set of latches.

A computer-readable medium encoded with a program for controlling the operation of a computer, the program comprising:

• a first set of instructions for causing the computer to identify a set of latches in a synthesized layout of sequential logic that exhibit flip flop output behavior;
• a second set of instructions for causing the computer to replace the set of latches with flip flops to generate a remodeled layout;
• and
• a third set of instructions for causing the computer to perform clock modeling on the remodeled layout,
• wherein the first set of instructions comprises:
• a first instruction for causing the computer to apply cone partitioning to the synthesized layout to determine a data fan-in cone and a first clock net for a test latch in the synthesized layout, wherein cone partitioning starts at a latch pin and expands out recursively to compile upstream logic until one of a primary input and a sequential logic gate is reached;
• and
• a second instruction for causing the computer to include the test latch in the set of remodeling-eligible latches if:
• the data fan-in cone does not include a primary input to the synthesized layout;
• the data fan-in cone does not include a first sequential logic gate driven by a second clock net that is not functionally equivalent to the first clock net;
• and
• the data fan-in cone does not include a second sequential logic gate that exhibits a first phase behavior that is equivalent to a second phase behavior of the test latch.

A computer-readable medium encoded with a program for controlling the operation of a computer, the program comprising:

• a first set of instructions for causing the computer to identify a set of latches in a synthesized layout of sequential logic that exhibit flip flop output behavior;
• a second set of instructions for causing the computer to replace the set of latches with flip flops to generate a remodeled layout;
• and
• a third set of instructions for causing the computer to perform clock modeling on the remodeled layout,
• wherein the first set of instructions comprises:
• a first instruction for causing the computer to apply cone partitioning to the synthesized layout to determine a data fan-in cone and a first clock net for a test latch in the synthesized layout, wherein cone partitioning starts at a latch pin and expands out recursively to compile upstream logic until one of a primary input and a sequential logic gate is reached;
• and
• a second instruction for causing the computer to include the test latch in the set of remodeling-eligible latches if:
• the data fan-in cone does not include a primary input to the synthesized layout;
• the data fan-in cone does not include a first sequential logic gate driven by a second clock net that is not identical to the first clock net;
• and
• the data fan-in cone does not include a second sequential logic gate that exhibits a first phase behavior that is equivalent to a second phase behavior of the test latch.

A computer-readable medium encoded with a program for controlling the operation of a computer, the program comprising:

• a first set of instructions for causing the computer to identify a set of latches in a synthesized layout of sequential logic that exhibit flip flop output behavior;
• a second set of instructions for causing the computer to replace the set of latches with flip flops to generate a remodeled layout;
• and
• a third set of instructions for causing the computer to perform clock modeling on the remodeled layout,
• wherein the first set of instructions comprises:
• a first instruction for causing the computer to apply cone partitioning to the synthesized layout to determine a data fan-in cone and a clock net for each latch in the synthesized layout, wherein cone partitioning starts at a latch pin and expands out recursively to compile upstream logic until one of a primary input and a sequential logic gate is reached;
• a second instruction for causing the computer to exclude a first set of latches from the set of remodeling-eligible latches, wherein the data fan-in cone of each of the first set of latches includes a primary input to the synthesized layout;
• a third instruction for causing the computer to exclude a second set of latches from the set of remodeling-eligible latches, wherein the data fan-in cone of each of the second set of latches includes at least one sequential logic gate driven by a first clock net, wherein the first clock net is not equivalent to a second clock net driving the each of the second set of latches;
• and
• a fourth instruction for causing the computer to exclude a third set of latches from the set of remodeling-eligible latches, wherein the data fan-in cone for each of the third set of latches includes a first sequential logic gate having a first phase behavior that is equivalent to a second phase behavior of the each of the third set of latches.