Enhanced verification by closely coupling a structural satisfiability solver and rewriting algorithms

A data processing system comprising:

• a processor;
• data storage coupled to the processor;
• and
• program code within the data storage that, when executed by the processor, causes the data processing system to perform:
• initializing a first variable to limit a rewrite time for rewrite operations with respect to an initial design by a rewriting module;
• initializing a second variable to limit a time for satisfiability solver operations with respect to said initial design by a satisfiability solver module;
• initializing a third variable to limit a maximum number of rewrite iterations with respect to said initial design;
• calling a timer to track said rewrite time;
• running a local logic rewriting operation on said initial design with said rewriting rewrite module;
• in response to determining that all of all targets for an said initial design netlist are not solved, determining whether a rewrite time is expired;
• in response to determining that said rewrite time is not expired, running AND refactoring;
• and
• in response to determining that said rewrite time is not expired, running XOR refactoring.

A program product, comprising:

• a non-transitory computer readable storage medium;
• and
• program code, stored within the computer-readable storage medium, that when processed by a computer, causes said computer to perform:
• initializing a first variable to limit a rewrite time for rewrite operations with respect to an initial design by a rewriting module;
• initializing a second variable to limit a time for satisfiability solver operations with respect to said initial design by a satisfiability solver module;
• initializing a third variable to limit a maximum number of rewrite iterations with respect to said initial design;
• calling a timer to track said rewrite time;
• running a local logic rewriting operation on said initial design with said rewriting module;
• in response to determining that all of all targets for an initial design netlist are not solved, determining whether a rewrite time is expired;
• in response to determining that said rewrite time is not expired, running AND refactoring;
• and
• in response to determining that said rewrite time is not expired, running XOR refactoring.