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

如圖，其中，LEC1和LEC4是RTL vs Netlist，LEC2和LEC3是Netlist vs Netlist。我們把RTL叫做參考（Ref），Netlist叫做實(shí)現(xiàn)（Imp）。做LEC就是以參考為準(zhǔn)，檢查實(shí)現(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，

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

注意1：lib庫有很多corner（wc、tc、bc），因?yàn)槲覀冎魂P(guān)心邏輯是否一致（不太關(guān)心時(shí)序），所以這個(gè)地方用哪一個(gè)corner的庫無所謂。

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

RTL vsNetlistLEC的原理

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

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

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

因?yàn)檫壿嬪F的大小是有限的，所以很容易用數(shù)學(xué)遍歷的方法來證明兩個(gè)邏輯錐等價(jià)。

RTL vsNetlistLEC的難點(diǎn)

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

難點(diǎn)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;

審核編輯：湯梓紅