US 6,983,429 B2
Formal proof methods for analyzing circuit loading problems under operating conditions
David W. Selway, Phoenix, Ariz. (US); and Boubaker Shaiek, Phoenix, Ariz. (US)
Assigned to Bull HN Information Systems Inc., Billerica, Mass. (US)
Filed on Sep. 30, 2003, as Appl. No. 10/675,851.
Prior Publication US 2005/0071793 A1, Mar. 31, 2005
Int. Cl. G06F 17/50 (2006.01)
U.S. Cl. 716—1 2 Claims
OG exemplary drawing
 
1. A process for determining the optimum load driving capacity for a driving node 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 driving capacity;
C) if, during step B), it is determined that the total number of pass transistor loads is exceeds an absolute maximum, then:
1) to the logic equations of the logic circuit, adding logic equations which represent the sum of the pass transistor loads;
2) to the logic equations of the logic circuit, adding comparator logic equations to compare the number of pass transistors turned on from one to the absolute maximum;
3) using a formal proof program to analyze the logic circuit and determine which of the comparators have a true output;
4) identifying the comparator for the largest number which has a possible true output to determine the highest possible actual load; and
5) if necessary, adjusting the driving capacity of the driving node to handle the determined highest possible actual load.