使用ESP-CV进行存储器位图验证

仿真设置非常困难。每个实例都需要一个序列将实例初始化到可以进行读取的状态。除时钟和地址之外的顶层引脚应绑定到初始化文件中的值，其中一些引脚需要被固定连接。还可能需要在原始网表 Netlist中替换某些单元为定制单元，以便数字仿真器能够正确仿真这些单元的行为。

Page 5

大型存储器实例运行时间长是该方法的另一个缺点。对于一个512K的ROM，在Linux机器上的测试速度约为6位/秒——彻底测试整个存储器需要24小时。

3.0 ESP-CV

ESP-CV是一个用于测试功能等效性的符号仿真 Symbolic Simulation工具，是定制化和重复性设计模块（如存储器）的流行选择。

3.1 符号仿真

传统的功能等效性检查 Equivalence Checking工具可分为两类：传统逻辑仿真和基于锥体的形式等效性检查 Formal Equivalence Checking。两者都不适用于大型存储器实例。传统逻辑仿真耗时较长，通常无法覆盖大型存储器模块的整个地址和位空间。形式等效性检查工具对RTL编码风格有特定限制，这意味着它无法处理存储器模块的HDL行为模型。其处理晶体管模型（如存储器模块中的灵敏放大器 Sense Amplifier）的能力也有限。

符号仿真 Symbolic Simulation应运而生，它是逻辑仿真和形式等效性检查的混合体。符号仿真仍然像逻辑仿真一样是事件驱动的，但它使用符号而不是1和0作为输入。它将符号在电路中传播，在输出端生成方程，然后对生成的方程进行形式分析。

借助符号仿真，可以克服形式等效性检查的RTL和电路限制，以及逻辑仿真的容量和全面性问题。

3.2 Verilog门级网表

ESP-CV是一个强大的符号仿真 Symbolic Simulation工具。它可以直接读取Verilog行为模型和SPICE 模型网表，并比较存储器模块的两种视图以查看它们是否等效。

ESP-CV流程的一个重要步骤是该工具可以直接读取SPICE网表，将其转换为相应的Verilog门级网表 Netlist，并比较Verilog行为模型和生成的Verilog门级网表是否等效。在读取SPICE网表并将其转换为Verilog门级网表的过程中，它还具有自动识别位单元的能力。这对存储器位图验证 Memory Bitmap Verification非常重要。

4.0 新方法论

ESP-CV主要用于存储器的Verilog参考模型和SPICE网表之间的形式等效性检查 Formal Equivalence Checking。通过专门化的初始化和在存储器位单元中适当插入$display任务，它还可以用于打印输出逻辑到物理的位图信息。这些逻辑到物理的位图信息可以进行后处理，以验证拼接引擎生成的节点位图。

Page 6

总体方法可描述如下： 1. 将所有位单元初始化为逻辑1。

   set_net_initial_value -i -design i_117CC -delay 10 -value 1 CORED
   

2. 在实现存储器核心单元中添加以下内容后，通过测试平台执行一个符号写周期：

   always @(wordline)
     if (bitline==0) $display("%m addr=%b data=%b", addr, data);
   

3. 使用脚本处理生成的输出行，这些行显示了单元实例名称（来自%m）、地址，以及符号数据字段中的"0"或"1"指示该单元对应数据字中的哪个位。例如：

   inno_tb_top.xtor.XI5.XBANK0.X0.X7 addr=111 data=sssssss0
   inno_tb_top.xtor.XI5.XBANK1.X0.X7 addr=111 data=sssss0ss
   ...
   

请注意，由于所有CORED网络都被初始化为1，而位图信息仅在bitline为0时打印输出，因此每当数据位中出现0时，该数据位为真值；每当出现1时，该数据位为互补位（即数据位经过位翻转）。

具体示例（使用ESP Tcl Shell）和RA1设计：（这是一个1024-by-4的存储器，即10个地址位，每个字宽4位。）

启动ESP Tcl Shell：

esp_shell

读取Verilog、SPICE并设置引脚属性：

read_verilog   -r i_117.v
set_top_design -r i_117

set_device_model -i -type PMOS hvtpfet
set_device_model -i -type NMOS hvtnfet
set_device_model -i -type PMOS dqlpfetpu
set_device_model -i -type NMOS dqlnfetwl
set_device_model -i -type NMOS dqlnfetpd
set netlist_bus_extraction_style {%s[%d]}
read_spice     -i i_117.lvsCdl
set_top_design -i i_117
match_design_ports
set_testbench_pin_attributes CLK -func Clock   -value High
set_testbench_pin_attributes A   -func Address -value High
set_testbench_pin_attributes D   -func Data    -value High
set_testbench_pin_attributes WEN -func Write   -value Low
set_supply_net_pattern -i VDDPE -type real -logic 1
set_supply_net_pattern -i VDDCE -type real -logic 1
set_supply_net_pattern -i VSSE -type real -logic 0
set_net_initial_value -i -design i_117CC -delay 10 -value 1 CORED

Page 7

创建约束以设置一个写周期并仅允许一个符号写周期：

set_constraint -set {1'b0} {CEN}
set_constraint -set {1'b1} {TEN}
set_constraint -set {1'b1} {RETN}
set_constraint -set {1'b1} {BEN}
set_constraint -set {3'b0} {EMA}
set_constraint -set {1'b0} {TCEN}
set_constraint -set {1'b0} {TWEN}
set_constraint -set {10'b0} {TA}
set_constraint -set {4'b0} {TD}
set_constraint -set {4'b0} {TQ}

set_constraint -cycle {"BINCYCLE1"} -set {1'b1}                 {WEN}
set_constraint -cycle {"SYMCYCLE1"} -set {1'b0}                 {WEN}

写出ESP数据库文件。请注意，您需要在运行验证之前执行此操作，因为之后无法写出。如果使用GUI：配置 > "Generate switch level verilog netlist"，然后填入输出文件名并选择Spice仿真模式：rcdelays

write_esp_db -i i_117.gv

向MEMCELL模块添加$display以创建i_117.gv.mod1文件，然后用此文件覆盖原始ram.gv文件。此示例将添加的实际代码行：

always @(WL) begin
  if (BL==0) begin
    $display("%m addr=%b data=%b", inno_tb_top.A, inno_tb_top.D);
  end
end

exec cp -fp i_117.gv      i_117.gv.mod0
exec cp -fp i_117.gv.mod1 i_117.gv
set testbench_style symbolic
set testbench_binary_cycles {0}
set testbench_symbolic_cycles {1}
set testbench_flush_cycles {0}
write_testbench i_117

仿真并报告结果：

verify
report_log

quit

后处理输出。将有4096行（4K x 4位/字 = 16384位），如下所示：

inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI11.XI1.XI0 addr=0100100000 data=ss0s
inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI13.XI1.XI0 addr=0101100000 data=ss0s
inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI15.XI1.XI0 addr=0110100000 data=ss0s

Page 8

inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI17.XI1.XI0 addr=0111100000 data=ss0s
inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI19.XI1.XI0 addr=1000100000 data=ss0s
inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI21.XI1.XI0 addr=1001100000 data=ss0s
inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI23.XI1.XI0 addr=1010100000 data=ss0s
inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI25.XI1.XI0 addr=1011100000 data=ss0s
...
inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI11.XI33.XI0 addr=0100100000 data=sss0
inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI13.XI33.XI0 addr=0101100000 data=sss0
inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI15.XI33.XI0 addr=0110100000 data=sss0
inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI17.XI33.XI0 addr=0111100000 data=sss0
inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI19.XI33.XI0 addr=1000100000 data=sss0
inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI21.XI33.XI0 addr=1001100000 data=sss0
inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI23.XI33.XI0 addr=1010100000 data=sss0
inno_tb_top.xtor.XI0.XI3.XI0.XI0.XI25.XI33.XI0 addr=1011100000 data=sss0
...

对于这个特定的RAM，它们表明XI0.XI3.XI0.XI0.XI11.XI1.XI0单元对应地址0100100000和数据总线位1，而XI0.XI3.XI0.XI0.XI11.XI33.XI0对应地址0100100000和数据总线位0，等等。

5.0 实现

- 首先，创建一个ESP-CV命令tcl文件。该文件基于prims.spc、电源、引脚属性和引脚约束的输入创建。引脚约束应设置为产生一个符号写周期，即所有控制引脚为二进制值，存储器使能且写使能。对于双端口SRAM，引脚约束应设置为确保一个端口正在写入，另一个端口正在读取。

- 接下来，创建并修改开关级Verilog网表。Verilog网表位单元应该已经通过以下命令进行了正确的初始化：

  set_net_initial_value -i -design  -delay 10 -value 1 CORED
  

  always @(WL) begin
    if (BL==0) begin
      $display("%m addr=%b data=%b", inno_tb_top.A, inno_tb_top.D);
    end
  end
  

- 使用tcl命令文件运行ESP-CV，并通过后处理日志文件获取位图信息。

  esp_shell -file run.tcl |& tee log
  grep "addr=" log |sort -k 2 > esp.bitmap
  

- 进行位图验证。遍历节点位图，对于节点位图中的每一行，尝试在ESP-CV位图中找到相应信息。例如，对于节点位图中的以下行：

  0x0 0 i1/i0_0/i1/i1/i0_1/cored_ i1/i0_0/i1/i1/i0_1/cored
  

Page 9

inno_tb_top.xtor.Xi1.Xi0_0.Xi1.Xi1.Xi0_1 addr=000 data=sssssss1

6.0 性能

使用ESP-CV，我们可以在仅一个仿真周期内完成位图验证，设置更加容易且运行时间更快。下表显示了ESP-CV与IRSIM在位图验证中的运行时间和内存使用比较：

7.0 局限性

该方法应适用于大多数存储器类型，但ROM除外。我们曾尝试在ROM上使用相同的方法，但不幸的是，由于ROM位单元的只读特性以及一个ROM位单元对应两个位单元的事实，ESP-CV只能给出完整的地址信息，而无法给出完全解码的数据位信息。这使我们无法完全验证ROM的逻辑位图 Logical Bitmap。

8.0 致谢

非常感谢Synopsys的David Hedges提供了关于ESP-CV流程的深刻见解。同时感谢Synopsys的Jeremy Poole和David Hedges审阅本文并提出修改意见。

9.0 参考文献

1. ESP-CV User Guider, June 2007

图片索引

本文共1张图片，存放于 SNUG_2008_SanJose_Chen_Microsoft_Word_chen_final_2_26doc_paper_images/ 目录。