Why Gate-to-Gate Comparison Fails in Formality with Multibit Flops?

From https://www.linkedin.com/pulse/why-gate-to-gate-comparison-fails-formality-multibit-flops-zheng-hpfqc

SVF (Automated setup file) files play a critical role in Logic Equivalence Checking (LEC), particularly in designs involving multibit flops. These files contain essential information about state elements, such as flip-flops, which influence how tools like Synopsys Formality interpret the netlist. When both the Reference and Implementation Netlists contain multibit flops, it's crucial to apply SVF files to each netlist individually to avoid issues.

The Issue with Synopsys Formality and SVF Application

In Synopsys Formality, SVF files are applied exclusively to the Implementation Netlist, even if multiple SVF files are provided. This is because Formality assumes by default that the LEC is performed between the RTL and the Netlist. This assumption becomes problematic when both the Reference and Implementation Netlists contain multibit flops, as these netlists may have different groupings or configurations. If an SVF file intended for the Reference Netlist is incorrectly applied to the Implementation Netlist, it can cause mismatches during LEC, leading to failures.

For example, as shown in Figure 1:

The Implementation SVF file indicates that flip-flops reg[2] to reg[5] are merged into a four-bit multibit flop in the Implementation Netlist.
The Reference SVF file indicates that flip-flops reg[0], reg[1], reg[6], and reg[7] are merged into a different four-bit multibit flop in the Reference Netlist.

Figure 1: SVF files for both Implementation and Reference

These SVF files should be applied to their respective netlists - Implementation SVF to the Implementation Netlist and Reference SVF to the Reference Netlist. However, since Synopsys Formality applies SVF files only to the Implementation Netlist, the tool cannot correctly map the multibit flops from the Reference SVF file to the Reference Netlist. This misalignment can cause LEC failures because the multibit configurations are not accounted for as intended.

SVF files are vital in multibit flop designs as they guide the LEC tool in understanding how individual flip-flops are grouped into multibit flops. Some naming change in a flop's name within an SVF file implies a new multibit flop mapping, which must be correctly interpreted during LEC. Misinterpreting this mapping can lead to incorrect comparisons between the Reference and Implementation Netlists.

Figure 2: Changing name implies multibit flop

GOF ECO's solution

GOF ECO use the -imp and -ref options in the read_svf command to apply SVF files to the Implementation and Reference Netlists separately, ensuring that each design receives the correct multibit flop mapping information.

example

Two SVF files for Reference and Implementation netlists

# GOF ECO script, the API sequence should be strictly followed
use strict; # To catch script syntax issue
# Setup ECO name 'auto_svf'
setup_eco("auto_svf_example");
read_library("/lib/5nm/tsmc_typ_85c_078v_svt.lib"); # Read in standard library 1
read_library("/lib/5nm/tsmc_typ_85c_078v_lvt.lib");# Read in standard library 2
read_svf("-ref", "/proj/ai_acc/new_syn/reference.svf.txt"); # SVF file must be loaded before read_design, and must be in text format
read_svf("-imp", "/proj/ai_acc/syn/implementation.svf.txt"); # SVF file must be loaded before read_design, and must be in text format
read_design("-ref", "/proj/ai_acc/new_syn/reference.gv"); # Read in Reference Netlist file after new synthesis
read_design("-imp", "/proj/ai_acc/post/implementation.gv"); # Read in Implementation Netlist file Which is under ECO
set_top("topmod");# Set the top module that ECO is working on
set_ignore_output("scan_out*");
set_pin_constant("scan_enable", 0);
set_pin_constant("scan_mode", 0);
fix_design();
save_session("auto_svf_session"); # Save a session for future restoration
report_eco(); # ECO report
check_design("-eco");# Check if the ECO causes any issue, like floating
write_verilog("/proj/ai_acc/eco/eco_verilog.v");# Write out ECO result in Verilog
# You need to change the file names, instance names and port names in the script

Conclusion

In summary, when both the Reference and Implementation Netlists have multibit flops, it is essential that their respective SVF files be applied correctly. However, tools like Synopsys Formality, which apply SVF files only to the Implementation Netlist, can struggle with this, leading to LEC failures. Understanding and addressing this limitation is crucial for successful equivalence checking in designs with multibit flops.