Shift Left Detection of Logic Equivalence Abort Points via RTL Linter
DescriptionThis paper discusses shift left technologies to identify hard logic equivalence problems at RTL stage and provide guidance to the RTL designer or the implementation tools in terms of synthesis constraints to significantly reduce the equivalence checking time and improve performance and coverage

Issues with logic equivalence aborts?

- Equivalence checking is NP-complete problem, and it may happen that verification on some points may not converge and logic equivalence tools may abort with respect to certain end points
- The primary reason for this is the lack of similarity between the RTL and the optimized Netlist
- Resolving these hard points can be a challenge, and in some cases, re-synthesis by disabling some class of synthesis optimizations can help verification
- Detecting hard points during verification can be too-late as RTL may be frozen at that design-stage
- Customers are looking for "early” detection (during RTL Linting) of hard to verify points, thus creating a process where RTL-changes and synthesis constraints can be identified at linting stage to ensure reliable [synthesis + verification] results

Lack of synergy between front-end static linters, equivalence checkers and implementation tools

- Missing analysis of complex data paths with don't cares at an earlier stage. No handshake with implementation tools w.r.t synthesis QoR
- Need to improve the regular lint flow by smartly catching and reporting accurate aborts points from logic equivalence early at the RTL level
- Need an innovative way to generate and pass synthesis constraints that will prevent aggressive optimizations on certain cones
Event Type
TimeMonday, July 10th3:30pm - 3:45pm PDT
Location2012, 2nd Floor