LOGIC MODIFICATION SYNTHESIS

Two circuits, an original and a modified, are being recognized, with the original circuit having a first logic and the modified circuit having a second logic. The second logic contains at least one desired logic change relative to the first logic. An equivalence line is detected in the original circuit such that the first and second logic are equivalent from the circuit inputs to the equivalence line. At least one point of change is located amongst the logic gates that are neighboring the equivalence line. The points of change are accepted as verified if an observability condition is fulfilled. The observability condition is checked within a Boolean Satisfiability (SAT) formulation. Substitute logic for the verified points of change is derived using SAT and Boolean equation solving techniques, in such manner that the first logic becomes equivalent to the second logic.