RTL与网表的一致性检查

在芯片设计的中间和最后阶段，比如综合、DFT、APR、ECO等阶段，常常要检查设计的一致性。也叫逻辑等价性检查（Logic Equivalence Check），简称LEC。

如图，其中，LEC1和LEC4是RTL vs Netlist，LEC2和LEC3是Netlist vs Netlist。我们把RTL叫做参考（Ref），Netlist叫做实现（Imp）。做LEC就是以参考为准，检查实现是否与参考一致。做LEC检查的目的是用formal的方法来保证逻辑一致。

RTL vsNetlist LEC的准备

RTL vs Netlist LEC的输入文件有：Lib库、RTL、网表。

RTL vsNetlistLEC的流程

第一步：读入Library库， 第二步：读入RTL， 第三步：读入Netlist， 第四步：设置option， 第五步：elab RTL，

第六步：运行lec检查。

注意1：lib库有很多corner（wc、tc、bc），因为我们只关心逻辑是否一致（不太关心时序），所以这个地方用哪一个corner的库无所谓。

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

RTL vsNetlistLEC的原理

在读入RTL和网表后，工具先建立内部数据库，再进行关键点映射（Keypoint Mapping）。关键点就是DFF的输入pin、blackbox的输入pin、顶层的输入port。我们可以把整个设计分割成若干个以关键点为终点的逻辑锥（如下图）。这些逻辑锥的起点可能是顶层的输入port、DFF的输出pin、blackbox的输出pin。

这些逻辑锥内部是单纯的组合逻辑，有N个输入，一个输出。可以用 Y = f (X1,X2, X3, ... , Xn)

来表示，所以可以通过数学的方法，来对RTL和Netlist的两个逻辑锥施加相同的一组激励，看逻辑锥的输出是否相同。

因为逻辑锥的大小是有限的，所以很容易用数学遍历的方法来证明两个逻辑锥等价。

RTL vsNetlistLEC的难点

由于RTL综合时的优化策略，做LEC有多个难点，总结一些如下： 难点1：ungroup，设计层次被打平 难点2：修fanout等design rules时，内部模块pin会被复制 难点3：DFF的复制，multi bitDFF 难点4：常量的传递和优化 难点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;

审核编辑：汤梓红