A process for determining the optimum load driving capacity for a driving node with a given total number of pass transistor loads in a logic circuit, comprising the steps of: A) extracting the logic equations of the logic circuit from a circuit description thereof; B) analyzing the fan-out of the driving node to determine if the total number of pass transistor loads is excessive compared to a predetermined load driving capacity of the driving node; characterized in that it further comprises the steps of: C) if, during step B), it is determined that the total number of pass transistor loads exceeds said predetermined load driving capacity, then: 1) to the extracted logic equations of the logic circuit, adding logic equations which represent the sum of loads through the pass transistors that are turned on; 2) to the extracted logic equations of the logic circuit, further adding comparator logic equations to compare an amount of the sum of loads through the pass transistors that are turned on with each load corresponding to a number of turned on pass transistors, said number increasing from one to the total number of pass transistor loads, wherein each comparator logic equation has a true output if and only if the amount of the sum of loads through the pass transistors that are turned on is greater than the load corresponding to the number of turned on pass transistors of this comparator logic equation; 3) using a formal proof program to analyze the added logic equations of steps C.1) and C.2), therefore determining which of the comparator logic equations of step C.2) can have a true output for any signal input combination in which the driving node can be active; 4) identifying the comparator logic equation corresponding to the largest number of turned on pass transistors which can have a true output as determined in step C.3) to determine the highest possible actual load; and 5) if necessary, adjusting the load driving capacity of the driving node to handle the determined highest possible actual load. A) extracting the logic equations of the logic circuit from a circuit description thereof; B) analyzing the fan-out of the driving node to determine if the total number of pass transistor loads is excessive compared to a predetermined load driving capacity of the driving node; C) if, during step B), it is determined that the total number of pass transistor loads exceeds said predetermined load driving capacity, then: 1) to the extracted logic equations of the logic circuit, adding logic equations which represent the sum of loads through the pass transistors that are turned on; 2) to the extracted logic equations of the logic circuit, further adding comparator logic equations to compare an amount of the sum of loads through the pass transistors that are turned on with each load corresponding to a number of turned on pass transistors, said number increasing from one to the total number of pass transistor loads, wherein each comparator logic equation has a true output if and only if the amount of the sum of loads through the pass transistors that are turned on is greater than the load corresponding to the number of turned on pass transistors of this comparator logic equation; 3) using a formal proof program to analyze the added logic equations of steps C.1) and C.2), therefore determining which of the comparator logic equations of step C.2) can have a true output for any signal input combination in which the driving node can be active; 4) identifying the comparator logic equation corresponding to the largest number of turned on pass transistors which can have a true output as determined in step C.3) to determine the highest possible actual load; and 5) if necessary, adjusting the load driving capacity of the driving node to handle the determined highest possible actual load. 1) to the extracted logic equations of the logic circuit, adding logic equations which represent the sum of loads through the pass transistors that are turned on; 2) to the extracted logic equations of the logic circuit, further adding comparator logic equations to compare an amount of the sum of loads through the pass transistors that are turned on with each load corresponding to a number of turned on pass transistors, said number increasing from one to the total number of pass transistor loads, wherein each comparator logic equation has a true output if and only if the amount of the sum of loads through the pass transistors that are turned on is greater than the load corresponding to the number of turned on pass transistors of this comparator logic equation; 3) using a formal proof program to analyze the added logic equations of steps C.1) and C.2), therefore determining which of the comparator logic equations of step C.2) can have a true output for any signal input combination in which the driving node can be active; 4) identifying the comparator logic equation corresponding to the largest number of turned on pass transistors which can have a true output as determined in step C.3) to determine the highest possible actual load; and 5) if necessary, adjusting the load driving capacity of the driving node to handle the determined highest possible actual load.