Checking equivalence between changes made in a circuit definition language and changes in post-synthesis nets

Apparatus for circuit design automation, comprising:

• a memory, which is configured to store an initial RTL definition of a design of a circuit, the design comprising multiple endpoints and first logical relations between sets of the endpoints, and an initial netlist of the circuit synthesized from the initial RTL definition, the netlist comprising second logical relations between the sets of the endpoints;
• a processor, which is coupled to receive, after synthesis of the initial netlist, an updated RTL definition, containing a design change relative to the initial RTL definition, and a corresponding updated netlist, and which is configured to automatically analyze the updated RTL definition and the updated netlist in the design automation computer so as to identify the first logical relations and the second logical relations that were changed in the updated RTL definition and the updated netlist, respectively, relative to the initial RTL definition and the initial netlist, and to issue a notification of the sets of the endpoints between which the first logical relations were changed without changes to the second logical relations and the sets of the endpoints between which the second logical relations were changed without changes to the first logical relations, and to automatically verify, for the sets of the endpoints between which both the first logical relations and the second logical relations were changed, an equivalence between the first logical relations in the updated RTL definition and the second logical relations in the updated netlist.

A computer software product, comprising a non-transitory computer-readable medium in which program instructions are stored, which instructions, when read by a computer, cause the computer to store an initial RTL definition of a design of a circuit, the design comprising multiple endpoints and first logical relations between sets of the endpoints, and an initial netlist of the circuit synthesized from the initial RTL definition, the netlist comprising second logical relations between the sets of the endpoints,

• wherein the instructions further cause the computer to receive, after synthesis of the initial netlist, an updated RTL definition, containing a design change relative to the initial RTL definition, and a corresponding updated netlist, and to automatically analyze the updated RTL definition and the updated netlist in the design automation computer so as to identify the first logical relations and the second logical relations that were changed in the updated RTL definition and the updated netlist, respectively, relative to the initial RTL definition and the initial netlist, and to issue a notification of the sets of the endpoints between which the first logical relations were changed without changes to the second logical relations and the sets of the endpoints between which the second logical relations were changed without changes to the first logical relations, and to automatically verify, for the sets of the endpoints between which both the first logical relations and the second logical relations were changed, an equivalence between the first logical relations in the updated RTL definition and the second logical relations in the updated netlist.