Chipress

It is not uncommon to see abort points during LEC. They are the key points that have not been proven either equivalent or non-equivalent based on the current tool settings, such as compare effort or compare algorithms.

There are several possible causes of abort points:

1. Don’t Care conditions, such as out-of-range index and X-assignments. They can increase complexity for comparison.
2. Resource sharing. Synthesis tools commonly look for opportunities for resource sharing, to achieve better PPA. As a result, such structural change can cause high complexity in comparing RTL with synthesis netlist.
3. XOR tree optimization. XOR trees are heavily used in logic like CRC modules. Synthesis tools may optimize XOR trees.
4. Key points with large logic cones.

Before debugging abort points, the first step is to resolve non-equivalent points. If there are both abort and non-equivalent points, one should address the latter first. When abort points are resolved, they will often be equivalent.

To get a full report of abort analysis, taking Cadence Conformal LEC as an example, use

 # This report focuses on the logic cone of abort points
 analyze_abort -verbose

Or

 # This report identifies abort points and their RTL file
 analyze_abort -source_diagnosis

For aborts due to resource sharing and XOR tree optimization, one can check the LEC log file after datapath analysis (“analyze_datapath -verbose” command).