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

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

RTL vsNetlist LEC的準(zhǔn)備

RTL vs Netlist LEC的輸入文件有：Lib庫、RTL、網(wǎng)表。

RTL vsNetlistLEC的流程

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

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

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

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

RTL vsNetlistLEC的原理

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

這些邏輯錐內(nèi)部是單純的組合邏輯，有N個輸入，一個輸出?？梢杂? Y = f (X1,X2, X3, ... , Xn)

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

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

RTL vsNetlistLEC的難點

由于RTL綜合時的優(yōu)化策略，做LEC有多個難點，總結(jié)一些如下： 難點1：ungroup，設(shè)計層次被打平 難點2：修fanout等design rules時，內(nèi)部模塊pin會被復(fù)制 難點3：DFF的復(fù)制，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;

審核編輯：湯梓紅