A method for circuit design automation includes receiving an initial RTL definition of a design of a circuit, and synthesizing an initial netlist of the circuit based on the initial RTL definition. After synthesizing the initial netlist, an updated RTL definition containing a design change and a corresponding updated netlist are received. The updated RTL definition and netlist are automatically analyzed to identify first and second logical relations that were changed in the RTL definition and netlist, respectively. A notification is issued of sets of the endpoints between which the first logical relations were changed without changes to the second logical relations or vice versa. For the sets of the endpoints between which both the first logical relations and the second logical relations were changed, the equivalence between the first and second logical relations is automatically verified.