Method and system for predicate selection in bit-level compositional transformations

A system in data processing system, said system comprising:

• means for selecting a first set containing a seed register;
• means for adding to a second set a result of a subtraction of a fanout of said first set from a fanin of said first set;
• means for setting a third set equal to a result of a subtraction of a fanin of said second set from a fanout of said second set;
• means for determining whether a combination of said first set and said third set is equivalent to said first set;
• and
• means for, in response to determining that said combination of said first set and said second set is not equivalent to said first set, returning a min-cut of said first set and said second set containing a minimal set of predicates between a first component and the logic to which said component fans out, wherein said logic is bordered by said second set.

A machine-readable medium having a plurality of instructions processable by a machine embodied therein, wherein said plurality of instructions, when processed by said machine, causes said machine to perform a method for verification, said method comprising:

• selecting a first set containing a seed register;
• adding to a second set a result of a subtraction of a fanout of said first set from a fanin of said first set;
• setting a third set equal to a result of a subtraction of a fanin of said second set from a fanout of said second set;
• determining whether a combination of said first set and said third set is equivalent to said first set;
• and
• in response to determining that said combination of said first set and said second set is not equivalent to said first set, returning a min-cut of said first set and said second set containing a minimal set of predicates between a first component and the logic to which said component fans out, wherein said logic is bordered by said second set.