Multi-Step LEC for Complex Functional ECO Debugging

Complex IC designs often require multiple steps to debug and verify equivalence between the RTL and gate-level netlists. In these cases, a multi-step LEC approach is essential to ensure accurate results and identify discrepancies effectively. By breaking down the debugging process into distinct stages, each comparison can deal with smaller structural changes. This is especially true when dealing with netlist ECOs involving multibit design.

Example Process for Multibit Flop Netlist Functional ECO

When performing functional ECO on a multibit flop netlist:

• RTL synthesized to single-bit netlist: The modified RTL is re-synthesized into a single-bit flop netlist to simplify debugging.
• Automatic ECO: The single-bit netlist is used as a reference to fix the multibit flop netlist.
• ECO Output: The ECOed multibit flop netlist is generated, ensuring smooth ECO execution.

However, achieving logic equivalence checking (LEC) success with this process can be challenging. Both Formality and Conformal LEC tools are employed, but Conformal LEC does not officially support SVF files, so Conformal is not efficient in comparing multibit flop netlists.

Multi-Step LEC Workflow

As shown in Figure 1, several methods have been tried:

• The first method, where RTL is directly compared with the ECOed netlist, fails with Formality in keypoint mapping.
• The second method has RTL compared to the synthesized single-bit netlist first by Formality, which passes. Then comparing the single-bit netlist to the ECOed multibit netlist by Conformal or Formality, which fails.
• The third method introduces an ECOed single-bit flop netlist, which is converted from the ECOed multibit flop netlist. It involves three comparisons and passes logic equivalence checking.

Figure 1: Multi-Step LEC for multibit design ECO

Convert Multibit Flop Netlist to Single-bit Flop Netlist

To address the LEC difficulty, the ECOed multibit flop netlist is converted into the ECOed single-bit flop netlist. This conversion allows for a more straightforward comparison with the synthesized single-bit flop netlist, and this comparison can use Conformal without SVF. The ECOed single-bit flop netlist is then used as a reference for the multibit flop netlist, ensuring accurate LEC results.

GOF ECO provides feature to convert multibit flop netlist to a single-bit flop netlist.

Example script for converting multibit flop netlist to single-bit flop netlist:

read_library("/lib/5nm/tsmc_typ_85c_078v_svt.lib"); # Read in standard library 1
read_svf("-imp", "multibit_netlist.svf.txt"); # SVF file must be loaded before read_design, and must be in text format
read_design("-imp", "ecoed_multibit_netlist.gv"); # Read in the ECOed multibit netlist
set_top("topmod");# Set the top module
set_force_singlebit(1);
set_force_split_multibit(1);
write_verilog("single_bit_netlist.gv");

Conclusion

Multi-step LEC is a crucial approach for debugging complex functional ECOs, especially those involving multibit flop netlists. By breaking down the debugging process into distinct stages and introducing a special middle-stage netlist, the ECOed single-bit flop netlist, which is converted from the ECOed multibit flop netlist, designers can ensure accurate LEC results and identify discrepancies effectively. This method can make the logic equivalence checking successful and save a lot of time in debugging the LEC process.