Patent ID: 8578311

Claim:
A computer-implemented method for determining a tight diameter bound of a netlist having at least one complex feed-forward component, the method comprising: a processor of a computing device identifying, within the netlist, one or more strongly connected components (SCCs), and identifying at least one SCC of the one or more SCCs that has a reconvergent fanin input with at least two input paths from the reconvergent fanin input having a different propagation delay to the SCC; in response to identifying the at least one SCC, computing an additive diameter for the at least one SCC, wherein the additive diameter includes a fanin additive diameter determined based on a propagation delay difference of the at least two input paths to the SCC; in response to the reconvergent fanin input to the SCC providing a binate function, computing a multiplicative diameter for the SCC utilizing a least common multiple (LCM) derived from one or more propagation delay differences across each reconvergent fanin input leading to the SCC; determining a final diameter bound over-approximation for the netlist by: computing a final additive diameter for the netlist, wherein the final additive diameter comprises the additive diameter of the reconvergent fanin input; responsive to the reconvergent fanin input providing a binate function, computing a final multiplicative diameter for the netlist, wherein the final multiplicative diameter is determined as a product of a cyclic multiplicative diameter of the SCC and a least common multiple (LCM) factor derived from one of more multiplicative diameters of one or more reconvergent fanin inputs; and adding the final additive diameter with the final multiplicative diameter to generate the diameter bound over-approximation for utilization during bounded model checking of the netlist.