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.
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:
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 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.
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 } }
Figure 2: Chang_names needs multibit restored
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_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
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.
