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