Challenges of Multibit Flops in Logic Equivalence Check and ECO
HEIDI ZHENG
Manager at NanDigits, Functional Netlist ECO, Functional Safety Fault Verification
Multibit flip-flops often create complexities during logic equivalence checks (LEC) and engineering change order (ECO) processes due to varying naming conventions adopted by different synthesis tools. For instance, as shown in Figure 1, a four-bit MBFF may have distinct naming styles in Cadence Genus compared to Synopsys Design Compiler after name transformation. Additionally, backend tools sometimes split MBFFs into single-bit flip-flops to address timing constraints. These factors significantly complicate the process of mapping key points accurately.
In LEC, MBFFs need to be mapped to single-bit flip-flops. However, the mapping of single-bit flip-flops to MBFFs between the Reference and Implementation netlists often varies. For example, as illustrated in Figure 1, the Implementation Netlist might contain a four-bit MBFF named a_reg_0_2_4_, while the Reference Netlist post-synthesis may instead have two separate two-bit MBFFs, named a_reg_0_1_ and a_reg_2_4_. Relying solely on naming conventions often fails to achieve correct MBFF-to-single-bit mapping. Although modern LEC and ECO tools implement advanced algorithms to manage partial mapping, complete and reliable mapping cannot always be guaranteed.
GOF Solutions for Multibit Flip-Flop Mapping
GOF provides a robust solution for precise and reliable key point mapping by utilizing text-mode SVF files generated by Design Compiler. These SVF files, which are encrypted by default, can be converted into a text-readable format using Formality. Additionally, GOF can interpret backend MBFF split/merge data and generate corresponding SVF files. By reading both the synthesis SVF file and the converted backend SVF file, GOF achieves accurate mapping of MBFFs to single-bit flip-flops.
For instance, Innovus generates a multi_bit_pin_mapping file that stores split and merge details of MBFFs. A GOF script can convert this file into an SVF text file for further processing.
read_library("libdir/art.lib");
set_multibit_blasting(0); # Disable multibit blasting
read_design('-imp', "imp_net.v");
set_top("the_top");
open(FIN, "./multi_bit_pin_mapping");
my $mbit_split = {};
my $mbit_merge = {};
while(<FIN>){
my ($from, $to) = (m/(\S+)\s+(\S+)/);
$from =~ s/\/\w+$//; # remove the pin
$to =~ s/\/\w+$//;
my ($module, $to_inst) = get_resolved($to);
my ($from_inst) = ($from =~ m/([^\/]+)$/);
my $libcell = get_ref($to);
gprint("get ref of $to as $libcell\n");
my $is_ff = is_seq($libcell, "-ff");
if($is_ff){
if(is_seq($libcell, "-bank")==0){
if(!exists $mbit_split->{$module}{$from_inst}){
$mbit_split->{$module}{$from_inst} = [];
}
if(grep($_ eq $to_inst, @{$mbit_split->{$module}{$from_inst}})==0){
gprint("Multibit split in $module $from_inst to $to_inst\n");
push @{$mbit_split->{$module}{$from_inst}}, $to_inst;
}
}else{
# Bank
if(!exists $mbit_merge->{$module}{$to_inst}){
$mbit_merge->{$module}{$to_inst} = [];
}
if(grep($_ eq $from_inst, @{$mbit_merge->{$module}{$to_inst}})==0){
gprint("Multibit merge in $module $from_inst to $to_inst\n");
push @{$mbit_merge->{$module}{$to_inst}}, $from_inst;
}
}
}
}
close(FIN);
my $svf = "";
foreach my $module (keys %$mbit_merge){
$svf .= "guide_multibit -design $module -type { svfMultibitTypeBank } \\\n";
$svf .= " -groups { \\\n";
foreach my $mbit_inst (keys %{$mbit_merge->{$module}}){
my $i_st = "";
my $cnt = 0;
foreach my $s_bit (@{$mbit_merge->{$module}{$mbit_inst}}){
$i_st .= " $s_bit 1";
$cnt++;
}
$i_st .= " $mbit_inst $cnt";
$svf .= "\t{ $i_st } \\\n";
}
$svf .= " }\n";
}
foreach my $module (keys %$mbit_split){
$svf .= "guide_multibit -design $module -type { svfMultibitTypeSplit } \\\n";
$svf .= " -groups { \\\n";
foreach my $mbit_inst (keys %{$mbit_split->{$module}}){
my $i_st = "";
my $cnt = 0;
foreach my $s_bit (@{$mbit_split->{$module}{$mbit_inst}}){
$i_st .= " $s_bit 1";
$cnt++;
}
$i_st = " $mbit_inst $cnt $i_st";
$svf .= "\t{ $i_st } \\\n";
}
$svf .= " }\n";
}
open(FOUT, ">backend_multibit.svf.txt");
print FOUT $svf;
close(FOUT);
Two SVF files for Implementation are loaded in the implementation read_svf:
read_svf("-ref", "reference.svf.txt");
read_svf("-imp", "implementation.svf.txt", "backend_multibit.svf.txt"); # Two SVF files are loaded
read_design("-ref", "reference.gv");# Read in Reference Netlist
read_design("-imp", "implementation.gv");# Read in Implementation Netlist Which is under ECO
Conclusion
Accurate multibit flip-flop mapping is critical for LEC and ECO success. GOF's integration of synthesis and backend data ensures reliable mapping, overcoming challenges caused by naming conventions and flop splitting.