Grouping and partitioning of properties for logic verification

1. A computer-implemented method for partitioning a netlist into grouped observable gates, the method comprising:

obtaining a netlist of a circuit comprising a plurality of observable gates;

grouping together a first observable gate and a second observable gate based on a portion of a fan-in logic of the first observable gate being equal to a portion of a fan-in logic of the second observable gate;

expanding the group to include a third observable gate, based on a first strongly connected component (SCC) in the group having a similarity greater than a first threshold to a second SCC in the fan-in logic of the third observable gate;

further expanding the group to include a fourth observable gate, based on the distance of a portion of the fan-in logic of the fourth observable gate from a fan-in logic of at least one observable gate in the group of observable gates; and

verifying the further expanded group of the circuit,

wherein an observable gate is a property to be verified, and wherein the further expanded group is verified independently from any other group of the circuit.

2. The computer-implemented method of claim 1 , wherein determining the first similarity comprises:

generating a first bit vector to represent the fan-in logic of the first observable gate, wherein each bit in the first bit vector is indexed to a respective position of a node of the fan-in logic of the first observable gate;

assigning a valid bit to each bit in the first bit vector indexed to a respective node comprising a support variable;

generating a second bit vector to represent the fan-in logic of the second observable gate, wherein each bit in the second bit vector is indexed to a respective position of a node of the fan-in logic of the second observable gate;

assigning a valid bit to each bit in the second bit vector indexed to a respective node comprising a support variable; and

determining whether the first bit vector is equal to the second bit vector.

3. The computer-implemented method of claim 2 further comprising:

generating a respective hash value for the first bit vector and the second bit vector; and

determining whether the first bit vector is equal to the second bit vector based on the respective hash values and a comparison of the first bit vector and the second bit vector.

4. The computer-implemented method of claim 2 , wherein determining the distance comprises:

generating a third bit vector to represent the fan-in logic of the fourth observable gate, wherein each bit in the third bit vector is indexed to a respective position of a node of the fan-in logic of the third observable gate;

assigning a valid bit to each bit in the third bit vector indexed to a respective node comprising a support variable;

converting the first bit vector and third bit vector to a respective mapped first bit vector and mapped second bit vector using a mapping sequence; and

determining whether the mapped first bit vector is equal to the second mapped bit vector based on a hash value of the mapped first bit vector and a hash value of the second mapped bit vector.

5. The computer-implemented method of claim 1 , wherein determining the similarity between the first SCC and the second SCC comprises:

weighting a value of the first SCC based on a count and a position of each register in the first SCC;

weighting a value of the second SCC based on a count and a position of each register in the second SCC; and

determining whether the first SCC and second SCC have a weighted value within a second threshold of a size of the netlist.

6. The computer-implemented method of claim 1 , wherein an observable gate is an endpoint for logic synthesis, and wherein the further expanded group is synthesized independently from any other group of the circuit.

7. A system for partitioning a netlist into grouped observable gates, the system comprising:

a memory having computer readable instructions; and

one or more processors for executing the computer readable instructions, the computer readable instructions controlling the one or more processors to perform operations comprising:

obtaining a netlist of a circuit comprising a plurality of observable gates;

grouping together a first observable gate and a second observable gate based on a portion of a fan-in logic of the first observable gate being equal to a portion of a fan-in logic of the second observable gate;

expanding the group to include a third observable gate, based on a first strongly connected component (SCC) in the group having a similarity greater than a first threshold to a second SCC in the fan-in logic of the third observable gate;

further expanding the group to include a fourth observable gate, based on the distance of a portion of a fan-in logic of the fourth observable gate from a portion of a fan-in logic of at least one observable gate in the group of observable gates; and

verifying the further expanded group of the circuit,

wherein an observable gate is a property to be verified, and wherein the further expanded group is verified independently from any other group of the circuit.

8. The system of claim 7 , wherein determining the first similarity comprises:

generating a first bit vector to represent the logic gate sequence of the first observable gate, wherein each bit in the bit vector is indexed to a respective position of a logic gate along the logic gate sequence of the first observable gate;

assigning a valid bit to each bit in the first bit vector in which the respective logic gate includes either a register or an input;

generating a second bit vector to represent the logic gate sequence of the second observable gate, wherein each bit in the bit vector is indexed to a respective position of a logic gate along the logic gate sequence of the second observable gate;

assigning a valid bit to each bit in the second bit vector in which the respective logic gate includes either a register or an input; and

determining whether the first bit vector is equal to the second bit vector.

9. The system of claim 8 the operations further comprising:

generating a respective hash value for the first bit vector and the second bit vector; and

determining whether the first bit vector is equal to the second bit vector based on the respective hash values and a comparison of the first bit vector and the second bit vector.

10. The system of claim 8 , wherein determining the distance comprises:

generating a third bit vector to represent the fan-in logic of the fourth observable gate, wherein each bit in the third bit vector is indexed to a respective position of a node of the fan-in logic of the third observable gate;

assigning a valid bit to each bit in the third bit vector indexed to a respective node comprising a support variable;

converting the first bit vector and third bit vector to a respective mapped first bit vector and a mapped second bit vector using a mapping sequence; and

determining whether the mapped first bit vector is equal to the second mapped bit vector, based on a hash value of the mapped first bit vector and a hash value of the second mapped bit vector.

11. The system of claim 7 , wherein determining the similarity comprises:

weighting a value of the first SCC based on a count and a position of each register in the first SCC;

weighting a value of the second SCC based on a count and a position of each register in the second SCC; and

determining whether the first SCC and second SCC have a weighted value within a second threshold of a size of the netlist.

12. The system of claim 7 , wherein an observable gate is an endpoint for logic synthesis, and wherein the further expanded group is synthesized independently from any other group of the circuit.

13. A computer program product for partitioning a netlist into grouped observable gates, the computer program product comprising a computer readable storage medium having program instructions embodied therewith, the program instructions executable by a processor to cause the processor to perform operations comprising:

obtaining a netlist of a circuit comprising a plurality of observable gates;

grouping together a first observable gate and a second observable gate based on a portion of a fan-in logic of the first observable gate being equal to a portion of a fan-in logic of the second observable gate;

expanding the group to include a third observable gate, based on a first strongly connected component (SCC) in the group having a similarity greater than a first threshold to a second SCC in the fan-in logic of the third observable gate;

further expanding the group to include a fourth observable gate, based on the distance of a portion of a fan-in logic of the fourth observable gate from a portion of a fan-in logic of at least one observable gate in the group of observable gates; and

verifying the further expanded group of the circuit,

wherein an observable gate is a property to be verified, and wherein the further expanded group is verified independently from any other group of the circuit.

14. The computer program product of claim 13 , wherein determining the first similarity comprises:

generating a first bit vector to represent the fan-in logic of the first observable gate, wherein each bit in the first bit vector is indexed to a respective position of a node of the fan-in logic of the first observable gate;

assigning a valid bit to each bit in the first bit vector in which the respective node comprises a support variable;

generating a second bit vector to represent the fan-in logic of the second observable gate, wherein each bit in the second bit vector is indexed to a respective position of a node of the fan-in logic of the second observable gate;

assigning a valid bit to each bit in the second bit vector in which the respective node comprises a support variable; and

determining whether the first bit vector is identical to the second bit vector.

15. The computer program product of claim 14 , wherein determining the distance comprises:

generating a third bit vector to represent the fan-in logic of the fourth observable gate, wherein each bit in the third bit vector is indexed to a respective position of a node of the fan-in logic of the third observable gate;

assigning a valid bit to each bit in the third bit vector indexed to a respective node comprising a support variable;

converting the first bit vector and third bit vector to a respective mapped first bit vector and a mapped second bit vector using a mapping sequence; and

determining whether the mapped first bit vector is equal to the mapped third bit vector based on a hash value of the mapped first bit vector and a hash value of the mapped second bit vector.

16. The computer program product of claim 13 further comprising:

generating a respective hash value for the first bit vector and the second bit vector; and

determining whether the first bit vector is equal to the second bit vector based on the respective hash values.

17. The computer program product of claim 13 , wherein determining the similarity comprises:

weighting a value of the first SCC based on a count and a position of each register in the first SCC;

weighting a value of the second SCC based on a count and a position of each register in the second SCC; and

determining whether the first SCC and second SCC have a weighted value within a second threshold of a size of the netlist.

18. The computer program product of claim 13 , wherein an observable gate is an endpoint for logic synthesis, and wherein the further expanded group is synthesized independently from any other group of the circuit.