Logic Equivalence Check Engine

LEC for Two Netlists

The built-in Logic Equivalence Check Engine checks the equivalence of two netlists. The speed and memory usage are similar to Conformal LEC and Formality.

Figure 1: GOF LEC Engine

Two netlists can be checked if they are equivalent by run_lec API.

# LEC script, run_example_lec.pl
use strict;
read_library("art.5nm.lib"); # Read in standard library
read_design('-ref', 'AI2021_top_syn.v'); # Read in the Reference Netlist, prelayout netlist
read_design('-imp', 'AI2021_top_pr.v'); # Read in the Implementation Netlist, postlayout netlist
set_top("AI2021_top"); # Set the top module
set_ignore_output("scan_out*");
set_pin_constant("scan_enable", 0);
set_pin_constant("scan_mode", 0);
my $non_equal = run_lec; # Run logic equivalence check on the two netlists
if($non_equal){
  gprint("LEC failed with $non_equal non-equivalent points");
}else{
  gprint("LEC passed");
}

Equivalent Nets Searching

In ECO process, GOF searches for equivalent nets in Implementation Netlist to optimize the patch circuit. The searching process is global.

Figure 2: Equivalent Nets Searching

Any two nets in the Reference and Implementation Netlists can be checked if they are equivalent. The API 'comare_nets' can be used to compare any two nets in Reference Netlist and Implementation Netlist.

Check equivalence of two nets in the reference and implementation netlist