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

Abstract

A method for performing verification includes selecting a first set containing a seed register and adding to a second set a result of a subtraction of a fanout of the first set from a fanin of the first set. A third set is rendered equal to a result of a subtraction of a fanin of the second set from a fanout of the second set, and whether a combination of the first set and the third set is equivalent to the first set is determined. In response to determining that the combination of the first set and the second set is not equivalent to the first set, a min-cut of the first set and the second set containing a minimal set of predicates between a first component and the logic to which the component fans out, wherein the logic is bordered by the second set is returned.

1 . A method in data processing system, 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.    
   
   
       2 . The method of  claim 1 , further comprising the step of, in response to determining that said combination of said first set and said second set is not equivalent to said first set, adding to said first set the content of said third set.  
   
   
       3 . The method of  claim 1 , further comprising: 
 importing a design netlist containing one or more components;    computing one or more output functions for said one or more components;    generating one or more output equivalent state sets from said one or more output functions;    identifying one or more next-state functions for said one or more components;    producing one or more image equivalent state sets for said one or more next-state functions;    classifying one or more output-and-image equivalent state sets for said one or more image equivalent state sets and said one or more output equivalent state sets;    selecting one or more input representatives of said one or more equivalent input sets;    forming an input map from said one or more input representatives;    synthesizing said input map; and    injecting said input map back into said netlist to generate a modified netlist.    
   
   
       4 . The method of  claim 3 , further comprising the step of partitioning over one or more original states of said one or more components and one or more equivalence class inputs of said one or more components.  
   
   
       5 . The method of  claim 3 , further comprising the step of getting a preimage from said one or more next state functions and said one or more output-and-image equivalent states to generate a preimage of said one or more output-and-image equivalent states.  
   
   
       6 . The method of  claim 5 , wherein said step of producing one or more image equivalent states for said one or more next-state functions and said step of getting a preimage from said one or more next state functions and said one or more output-and-image equivalent states to generate said preimage of said one or more output-and-image equivalent states are performed in parallel.  
   
   
       7 . The method of  claim 5 , further comprising the step of performing verification of said modified netlist.  
   
   
       8 . 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.    
   
   
       9 . The system of  claim 8 , further comprising means for, in response to determining that said combination of said first set and said second set is not equivalent to said first set, adding to said first set the content of said third set.  
   
   
       10 . The system of  claim 8 , further comprising: 
 means for importing a design netlist containing one or more components;    means for computing one or more output functions for said one or more components;    means for generating one or more output equivalent state sets from said one or more output functions;    means for identifying one or more next-state functions for said one or more components;    means for producing one or more image equivalent state sets for said one or more next-state functions;    means for classifying one or more output-and-image equivalent state sets for said one or more image equivalent state sets and said one or more output equivalent state sets;    means for selecting one or more input representatives of said one or more equivalent input sets;    means for forming an input map from said one or more input representatives;    means for synthesizing said input map; and    means for injecting said input map back into said netlist to generate a modified netlist.    
   
   
       11 . The system of  claim 10 , further comprising means for partitioning over one or more original states of said one or more components and one or more equivalence class inputs of said one or more components.  
   
   
       12 . The system of  claim 10 , further comprising means for getting a preimage from said one or more next state functions and said one or more output-and-image equivalent states to generate a preimage of said one or more output-and-image equivalent states.  
   
   
       13 . The system of  claim 12 , wherein said means for producing one or more image equivalent states for said one or more next-state functions and said step of getting a preimage from said one or more next state functions and said one or more output-and-image equivalent states to generate said preimage of said one or more output-and-image equivalent states are employed in parallel.  
   
   
       14 . The system of  claim 12 , further comprising means for performing verification of said modified netlist.  
   
   
       15 . 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.    
   
   
       16 . The machine readable medium of  claim 15 , wherein said method further comprises the step of, in response to determining that said combination of said first set and said second set is not equivalent to said first set, adding to said first set the content of said third set.  
   
   
       17 . The method of  claim 15 , wherein said method further comprises: 
 importing a design netlist containing one or more components;    computing one or more output functions for said one or more components;    generating one or more output equivalent state sets from said one or more output functions;    identifying one or more next-state functions for said one or more components;    producing one or more image equivalent state sets for said one or more next-state functions;    classifying one or more output-and-image equivalent state sets for said one or more image equivalent state sets and said one or more output equivalent state sets;    selecting one or more input representatives of said one or more equivalent input sets;    forming an input map from said one or more input representatives;    synthesizing said input map; and    injecting said input map back into said netlist to generate a modified netlist.    
   
   
       18 . The machine readable medium of  claim 17 , wherein said method further comprises the step of partitioning over one or more original states of said one or more components and one or more equivalence class inputs of said one or more components.  
   
   
       19 . The machine readable medium of  claim 17 , wherein said method further comprises the step of getting a preimage from said one or more next state functions and said one or more output-and-image equivalent states to generate a preimage of said one or more output-and-image equivalent states.  
   
   
       20 . The machine readable medium of  claim 19 , wherein said step of producing one or more image equivalent states for said one or more next-state functions and said step of getting a preimage from said one or more next state functions and said one or more output-and-image equivalent states to generate said preimage of said one or more output-and-image equivalent states are performed in parallel.