In one implementation, the invention can be a computer-implemented method for generating an engineering change order (ECO) netlist for an integrated circuit (IC). The method includes performing a formal equivalence check between an implementation netlist and a reference netlist to identify one or more corresponding failed compare points in the implementation and reference netlists. The method further includes, for at least one failed comparison: (i) performing equivalence verifications based on fan-in cones for the failed compare points, to generate pin pass/fail information, (ii) tracing the fan-in cone for the reference netlist to generate ECO pin and cell information, and (iii) modifying the implementation netlist, based on (1) the pin pass/fail information, (2) cell connectivity information, (3) cell description information, and (4) the ECO pin and cell information, to generate the ECO netlist by adding one or more new ECO cells to the implementation netlist and appropriately connecting them.