Help file to pass Formality in logic equivalence checking

Original URL: https://www.linkedin.com/pulse/help-file-pass-formality-logic-equivalence-checking-heidi-zheng-pwjuc

The difficulty in large netlist ECO arises in successfully navigating logic equivalence checking, especially when undergoing RTL-to-ECO netlist equivalence checking with Formality, and without the aid of an updated SVF file. Many users of ECO tools may have faced situations where they had to abandon ECO results due to the challenges of passing logic equivalence checking under these circumstances.

In Figure 1, achieving success with Formality is relatively easier in scenario #1 when aided by the SVF file. However, it becomes more challenging in scenario #2 due to the absence of the SVF file. Some design companies may even impose the requirement to pass Formality using new RTL versus ECO netlist in scenario #3, marking the most demanding process. As Formality serves as a sign-off tool for many design companies, it has become a critical gating item in their ECO processes.

Figure 1: Logic equivalence checking by Formality in netlist ECO

GOF ECO offers a solution to address this issue. With its notably high success rate in netlist ECO and a flexible counterexample annotation feature for non-equivalence debugging, GOF ECO is capable of generating helpful files to facilitate passing Formality after the netlist ECO process.
Following ECO and GOF LEC, the generation of assistance files for Formality is demonstrated in the following code snippet.

#GOF ECO script
read_library("tsmc.lib");
read_design("-ref", "new_pre_layout.v");
read_design("-imp", "post_layout.v");
fix_design;
write_verilog("eco_netlist.v");
run_lec;
write_formality_help_files("eco_010323");

The API produces files such as eco_010323.config.tcl, with essential Formality commands like set_user_match, rewire_connection, and set_constant. Integrating this TCL file directly into the Formality script equips Formality with the necessary configurations to pass logic equivalence checking, specifically addressing the requirements of scenario #2 depicted in Figure 1.

#Formality script for netlist vs netlist
read_db -tech tsmc.db
read_verilog -r new_pre_layout.v
read_verilog -i eco_netlist.v
#Setup constraint
source eco_010323.config.tcl
match 
verify

To accommodate the #3 Formality process, the TCL file needs modification to align with RTL naming conventions for registers. In practice, the RTL in Formality might adopt a register naming style distinct from the netlist. For instance, the RTL may use "counter_reg[0]," while the synthesized netlist may alter it to "counter_reg_0_." Adjustments in the TCL file should be made to account for these variations in register naming.

#Formality script for RTL vs netlist
read_db -tech tsmc.db
set_svf the_svf_file
read_verilog -r new_rtl.v
read_verilog -i eco_netlist.v
source eco_010323.config.modified.tcl
match 
verify

GOF platform integrates four functional components: ECO, Formal, LEC and Debug. To access detailed information about GOF, please visit the website https://nandigits.com