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 multibit flip-flops mapping, 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

Synopsys Formality applies SVF files only to the Implementation Netlist, even when multiple SVF files are provided. This default behavior assumes an LEC comparison between RTL and Netlist. However, when comparing two netlists with different multibit flop configurations, applying the SVF file intended for the Reference Netlist to the Implementation Netlist causes mapping errors and LEC 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.

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.

Hidden rules in SVF file

SVF files define rules to help LEC tools group individual flip-flops into multibit flops correctly. For a single module instance, each multibit mapping requires both guide_multibit and guide_change_names pairs.

Consider a three-dimensional register array example:

guide_multibit -design { one_mod } -type { svfMultibitTypeBank } \
   -groups { { ar_reg[12][7][1] 1 ar_reg[13][7][1] 1 ar_reg[14][8][1] 1 ar_reg[16][9][1] 1 ar_reg[12,13:14,16][7,7,8,9][1] 4 } }
guide_change_names -design one_mod { {cell ar_reg[12,13:14,16][7,7,8,9][1] ar_reg_12_13_14_16__7_7_8_9__1_ } }

However, when a hierarchical module has multiple instances, the guide pairs in SVF file may become incomplete after uniquification. For example, if submod is uniquified into submod_0 and submod_1, each instance might contain only half of the required guide statements.

• submod_0 has guide_multibit but lacks guide_change_names.

• submod_1 only retains guide_change_names.

Incomplete guide, submod_0 and submod_1 have half of the pairs:

guide_multibit -design { submod_0 } -type { svfMultibitTypeBank } \
   -groups { { dd 1 cc 1 bb 1 aa 1 dd,,cc,,bb,,aa 4 } }
guide_change_names -design submod_1 { { cell dd,,cc,,bb,,aa dd__cc__bb__aa } }

Complete guide pairs must be restored for all modules to ensure accurate interpretation during LEC. Incorrect mapping can lead to discrepancies between the Reference and Implementation Netlists. Each uniquified module must include both guide_multibit and guide_change_names pairs for each multibit flop to create a comprehensive guide.

The recovered complete guide, submod_0 and submod_1 have the full pairs:

guide_multibit -design { submod_0 } -type { svfMultibitTypeBank } \
   -groups { { dd 1 cc 1 bb 1 aa 1 dd,,cc,,bb,,aa 4 } }
guide_multibit -design { submod_1 } -type { svfMultibitTypeBank } \
   -groups { { dd 1 cc 1 bb 1 aa 1 dd,,cc,,bb,,aa 4 } }
guide_change_names -design submod_0 { { cell dd,,cc,,bb,,aa dd__cc__bb__aa } }
guide_change_names -design submod_1 { { cell dd,,cc,,bb,,aa dd__cc__bb__aa } }

Applying SVF Files with GOF ECO

GOF ECO restores missing guide statements in uniquified designs. It processes SVF files by applying them separately to the Reference and Implementation Netlists. By using the -imp and -ref options, it ensures correct multibit mapping, recovers incomplete guide statements, and prevents mismatches.

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 out ECO result in Verilog
write_verilog("/proj/ai_acc/eco/eco_verilog.v");

Conclusion

Successful equivalence checking for designs with multibit flops requires applying SVF files correctly to both Reference and Implementation Netlists. Tools like Synopsys Formality, which apply SVF files only to the Implementation Netlist, face limitations that can lead to LEC failures. Proper understanding, complete guide restoration, and tools like GOF ECO help address these challenges effectively.