There are various reasons why non-equivalent points can arise in logic equivalence checking, including missing DFT constraints that generate false non-equivalent points, failures in key point mapping, or genuine non-equivalent points. To address this issue, GOF Debug offers a solution that involves using a combination of GUI and script to identify the root cause of non-equivalence when comparing netlist to netlist. Specifically, individual nets equivalence checking can be a valuable tool in pinpointing the underlying problem.
While logic equivalence checking between RTL and netlist is typically straightforward using an SVF file, comparing netlist to netlist after ECO can pose challenges. However, GOF simplifies the debugging process by examining the schematic, extracting logic fanin endpoints, and performing individual nets equivalence checking. This debugging process can be performed using a combination of GUI and script mode.
There are multiple methods for loading instances to a schematic in GOF. One way is to use the "sch" command in the run script, as shown in the following script.
Example script to load the failing points to a schematic:
The debug process can also begin after GOF LEC has completed and unexpected non-equivalent points emerge after the ECO command fixes the design. To do this, remove the "exit" command from the script and directly run the "sch" command after the GOF prompt appears to load the flop instances that are non-equivalent.
To load additional instances from both netlists onto the schematic, you can right-click on the flop and select "Load Instance Similar to" from the pop-up menu using the mouse.
Figure : Non-Equivalent flops from the two netlists
As part of the debugging process, you can select the D pin and then right-click to choose "List Flatten Fanin Endpoints" to confirm whether the flatten fanin points match between the two netlists. These fanin points refer to the primary input ports, flip-flops, or output ports of a black-box. This step can be helpful in identifying the root cause of the non-equivalence issue.
Figure 1: Do flatten Fanin Endpoints analysis
A pop window shows the flatten fanin endpoints for IMP netlist.
Figure 2: IMP Endpoints
Do the same for REF instance
Figure 3: REF Endpoints
When comparing two points for equivalence, their flatten fanin endpoints should typically match. However, if they do not match and the points are not equivalent, this can help pinpoint the root cause of the issue. Mismatching fanin endpoints may be due to failure in keypoints mapping, or missing DFT logic constraints. Nevertheless, it is not always the case that fanin endpoint mismatches will result in non-equivalence.
GOF offers an extremely useful feature called "individual nets equivalence check" that enables users to check the equivalence of nets between two netlists. This feature allows the user to check the equivalence of any two nets in the two netlists, which can be helpful in identifying the root cause of non-equivalence. By verifying individual net pairs one by one, the user can systematically narrow down the cause of the non-equivalence.
To perform the individual nets equivalence check in GOF, you can select two nets from the two netlists by holding down the "ctrl" key and clicking on the pins of both instances. Then, you can right-click and choose "Equivalence Check for ai vs ai".
Figure 4: Equivalence Check Command
Once you have performed the individual nets equivalence check in GOF, a pop-up window will display the results. If the result indicates that the nets are not equivalent, you can continue investigating the fanin of the non-equivalent nets. On the other hand, if the result shows that the nets are equivalent, you can move on to checking other nets.
Figure 5: Not Equivalent Result
If the checking is run in debug mode, a counter-example will be back-annotated to the schematic.
Figure 6: Debug non-equivalence by counter-example back-annotated
To further investigate the non-equivalent nets, you can expand the schematic by using the "Show until non-buffer on Schematic" feature. This feature loads all cells in the driver path until it reaches a non-buffer cell, which can be a fast way to expand the schematic.
Figure 7: Use Fast Schematic Way
The "Show until non-buffer on Schematic" feature loads all the buffers, inverters, and connectors in the driver path until it reaches a non-buffer cell, such as an XOR gate. This can be a quick way to expand the schematic and investigate the non-equivalent nets.
Figure 8: Fast Schematic Expanding Result
To expand the schematic and investigate the non-equivalent nets, you can use the "Show until non-buffer on Schematic" feature or click on the input pins with the mouse middle-button. Then, you can continue checking the equivalence of related nets and pins as you expand the schematic.
Figure 9: Expanding Schematic
In cases where the equivalence check shows that two nets, such as 'zzsx' to 'zzsx', are non-equivalent, you can investigate further to identify the root cause. For example, the non-equivalence may be due to one driver being an XOR gate while the other driver is an OR gate, as seen in this example.
Figure 10: Root Cause Found
There may be instances where the two logic cones of the comparing points are significantly different. In such cases, examining the equivalence of the module input ports can help isolate whether the issue is solely within the module or if it also stems from the combinational logic in other hierarchies.
One way to check all input ports in the current module using an example script is:
The equivalence or non-equivalence, as well as the inversion, of input ports between two netlists can offer insights for further debugging.
In conclusion, real cases of logic equivalence checking can be far more complicated than the example provided. However, there are various techniques available to assist in the debugging process, such as the use of the flatten fanin points checker and individual nets equivalence checking. Employing a combination of GUI and script can also be advantageous. While these methods may not solve every issue, they can certainly aid in identifying and resolving problems that arise during the equivalence checking process.
