在芯片設計的中間和最后階段，比如綜合、DFT、APR、ECO等階段，常常要檢查設計的一致性。也叫邏輯等價性檢查（Logic Equivalence Check），簡稱LEC。

如圖，其中，LEC1和LEC4是RTL vs Netlist，LEC2和LEC3是Netlist vs Netlist。我們把RTL叫做參考（Ref），Netlist叫做實現(xiàn)（Imp）。做LEC就是以參考為準，檢查實現(xiàn)是否與參考一致。做LEC檢查的目的是用formal的方法來保證邏輯一致。

RTL vsNetlist LEC的準備

RTL vs Netlist LEC的輸入文件有：Lib庫、RTL、網表。

RTL vsNetlistLEC的流程

第一步：讀入Library庫， 第二步：讀入RTL， 第三步：讀入Netlist， 第四步：設置option， 第五步：elab RTL，

第六步：運行l(wèi)ec檢查。

注意1：lib庫有很多corner（wc、tc、bc），因為我們只關心邏輯是否一致（不太關心時序），所以這個地方用哪一個corner的庫無所謂。

注意2：第一步就要讀入lib庫，不管RTL中有沒有手工例化庫里的stdcell。

RTL vsNetlistLEC的原理

在讀入RTL和網表后，工具先建立內部數(shù)據庫，再進行關鍵點映射（Keypoint Mapping）。關鍵點就是DFF的輸入pin、blackbox的輸入pin、頂層的輸入port。我們可以把整個設計分割成若干個以關鍵點為終點的邏輯錐（如下圖）。這些邏輯錐的起點可能是頂層的輸入port、DFF的輸出pin、blackbox的輸出pin。

這些邏輯錐內部是單純的組合邏輯，有N個輸入，一個輸出。可以用 Y = f (X1,X2, X3, ... , Xn)

來表示，所以可以通過數(shù)學的方法，來對RTL和Netlist的兩個邏輯錐施加相同的一組激勵，看邏輯錐的輸出是否相同。

因為邏輯錐的大小是有限的，所以很容易用數(shù)學遍歷的方法來證明兩個邏輯錐等價。

RTL vsNetlistLEC的難點

由于RTL綜合時的優(yōu)化策略，做LEC有多個難點，總結一些如下： 難點1：ungroup，設計層次被打平 難點2：修fanout等design rules時，內部模塊pin會被復制 難點3：DFF的復制，multi bitDFF 難點4：常量的傳遞和優(yōu)化 難點5：門控時鐘 難點6：DFF phase inversion

難點7：retiming

RTL vsNetlistLEC的GOF示例腳本

# LEC script
use strict;


# Step1: read library
read_library("art.5nm.lib"); 


#Step2:readrtl(Refdesign)
set_inc_dirs("-ref", "inc_dir_path/include");
set_define("-ref", "NO_SIMULATION", 1);
my @rtl_files = (
    "cpu_core.sv", 
    "mem_ctrl.sv", 
    "display_sys.sv", 
    "chip_top.sv");
read_rtl("-ref", @rtl_files); 


#Step3:readnetlist(ImpDesign)
read_design('-imp','chip_top.v');


#Step4:set options
set_top("CHIP_TOP"); 
set_ignore_output("scan_out*");
set_pin_constant("scan_enable", 0);
set_pin_constant("scan_mode", 0);


# Step5: elab rtl
elab_rtl(); # RTL processing


# Step6: Run LEC
run_lec;

審核編輯：湯梓紅