大规模集成电路验证

《大规模集成电路验证》由会员分享，可在线阅读，更多相关《大规模集成电路验证（120页珍藏版）》请在装配图网上搜索。

1、VLSI Design and Verification大 规 模 集 成 电 路 设 计 与 验 证VLSI Verfication大 规 模 集 成 电 路 验 证 验 证 部 分 的 授 课 内 容 除 VLSI设 计 之 外 的 全 部 内 容 均 是 验 证 设 计 vs. 验 证 (design vs. Verification) 验 证 vs. 测 试 (Verification vs. Test) 投 片 前 验 证 vs. 投 片 后 验 证 (Pre-Silicon vs. Post-Silicon) Verfication, Validation, Testing 参 考

2、 资 料 课 程 教 材 集 成 电 路 计 算 机 辅 助 设 计 与 验 证 实 践 /算 法 Hardware Design Verification: Simulation and Formal Method-Based Approaches. Prentice Hall PTR. ISBN: 0131433474 全 面 的 功 能 验 证 ： 完 整 的 工 业 流 程 Comprehensive Functional Verification: The Complete Industry Cycle Proceedings: DAC, DATE, HLDVT, ITC 验 证 部

3、 分 课 程 学 习 组 成 课 程 讲 授 | HOME实 验 作 业 考 试 掌 握 原 理 的 基 础 上 强 调 实 践 验 证 原 理 ， 工 具 算 法 原 理 工 具 Synopsys VCS, Cadence IUS/IES, Mentor ModelSIM IFV, ZeroIn, SpyGlass, Conformal, Fomality DC, RC, ICC, Encounter, Tessent Office Hour 唐 遇 星 ， 副 研 究 员 微 电 子 与 微 处 理 器 研 究 所 微 处 理 器 研 究 室 619 Monday Tuesday: 20:

4、00 22:00 and weekend 302 计 算 机 工 厂 停 车 场 北 楼 Agenda Part 0. Welcome Part 1. Verfication Introduction Part 2. Testbench Simulation Tool Part 3. Testbench Construction and OpenSPARC Part.0 Welcome Welcome 领 域 Welcome 校 园 Welcome 课 程 Part.1 Introduction What?什 么 是 验 证 ？ Why? 为 什 么 要 验 证 ？ How? 如 何 开 展

5、验 证 ？ 验 证 包 括 哪 些 内 容 主 要 的 验 证 方 法 验 证 的 困 境 What is Design Verification什 么 是 验 证 The Opposite of Design Design: Make/Implement sth that you want Verification: Make sure that sth is what you want(correct) 确 保 设 计 符 合 原 始 设 计 需 求 与 目 标 功 能 正 确 ， 性 能 达 标 ， 功 耗 、 良 率 和 成 本 符 合 要 求 VLSI团 队 分 工 Design T

6、eam input 3:0 a, b;input c_in;output 3:0 sum;output c_out;assign c_out, sum = a + b + c_in;endmodule Simulation Exampleadder4b(DUT) a3:0b3:0 sum3:0c_out44c_in 4t_adder4b Testbench timescale 1ns /1ns / time_unit/time_precisionmodule t_adder4b; reg8:0 stim; / inputs to DUT are regswire3:0 S; / outputs

7、 of DUT are wires wire C4;/ instantiate DUTadder4b(S, C4, stim8:5, stim4:1, stim0);/ stimulus generationinitial begin stim = 9b000000000; / at 0 ns #10 stim = 9b111100001; / at 10 ns #10 stim = 9b000011111; / at 20 ns #10 stim = 9b111100010; / at 30 ns #10 stim = 9b000111110; / at 40 ns #10 $stop; /

8、 at 50 ns stops simulation endendmodule see “response” to each of these input vectorsUUTBehav.Verilog:“do this once” timing control for simulation Testbench Requirements Instantiate the Design Under Test (DUT) Provide input to that unit Usually a number of different input combinations! Watch the “re

9、sults” (outputs of DUT) Can watch Wave window Can print out information to the screen or to a file timescale 1ns /1ns / time_unit/time_precisionmodule t_adder4b; reg8:0 stim; / inputs to DUT are regswire3:0 S; / outputs of DUT are wires wire C4;/ instantiate DUTadder4b(S, C4, stim8:5, stim4:1, stim0

10、);/ monitor statementinitial $monitor($time, C4, S, stim8:5, stim4:1, stim0);/ stimulus generationinitial begin stim = 9b000000000; / at 0 ns #10 stim = 9b111100001; / at 10 ns #10 stim = 9b000011111; / at 20 ns #10 stim = 9b111100010; / at 30 ns #10 stim = 9b000111110; / at 40 ns #10 $stop; / at 50

11、 ns stops simulation endendmodule Exhaustive Simulation 综 合 后module adder4b ( sum, c_out, a, b, c_in ); output 3:0 sum; input 3:0 a,b; input c_in; output c_out; wire carry1 , carry2 ,carry3 ; ADD32 U1_0 ( .A(a0), .B(b0), .CI(c_in), .CO(carry1 ), .S(sum0) ); ADD32 U1_1 ( .A(a1), .B(b1), .CI(carry1 ),

12、 .CO(carry2 ),.S(sum1) ); ADD32 U1_2 ( .A(a2), .B(b2), .CI(carry2 ), .CO(carry3 ), .S(sum2) ); ADD32 U1_3 ( .A(a3), .B(b3), .CI(carry3 ), .CO(c_out), .S(sum3) );endmodulemodule ADD32 (A, B, CI, CO, S); input A,B,CI; output CO,S; and (net_1, CI, B); and (net_2, CI, A); and (net_3, B, A); or ( CO, net

13、_1, net_2, net_3); xor (S, CI, B, A);endmodule 如 何 验 证 综 合 后 网 表 的 正 确 性 ？ Consistency: same testbench at each level of abstractionBehavioral Gate-level Design(Post-layout) Gate-level Design(Pre-layout) RTL DesignTestbench Simulation 方 法 1： Gate-level simulation Given two designs, prove that for all

14、 possible input stimuli their corresponding outputs are equivalentDesign ADesign B =?Input Yes/NoProduct Machine 2： 例 2 ： 交 通 灯 控 制 器 Guarantee no collisions：It is never possible that all traffic lights are green Guarantee eventual service Eventually, each traffic light will become greenE S N Verilo

15、g programmodule main (N_SENSE,S_SENSE,E_SENSE,N_GO,S_GO,E_GO); input N_SENSE, S_SENSE, E_SENSE; output N_GO, S_GO, E_GO; reg NS_LOCK, EW_LOCK, N_REQ, S_REQ, E_REQ; /* set request bits when sense is high */ always begin if (!N_REQ end always begin if (!S_REQ end always begin if (!E_REQ end /* control

16、ler for North light */ always begin if (N_REQ) begin wait (!EW_LOCK); NS_LOCK = 1; N_GO = 1; wait (!N_SENSE); if (!S_GO) NS_LOCK = 0; N_GO = 0; N_REQ = 0; end end/* South light is similar . . . */ /* Controller for East light */ always begin if (E_REQ) begin EW_LOCK = 1; wait (!NS_LOCK); E_GO = 1; w

17、ait (!E_SENSE); EW_LOCK = 0; E_GO = 0; E_REQ = 0; end end 如 何 验 证 ？ 方 法 2： 模 型 检 验Traffic LightControllerDesign“ I t i s n e v e r possible to have a green light for both N-S and E-W.” ModelChecker TrueFalse+ Counterexample方 法 1： 模 拟 Safety (no collisions) AG (E_Go (N_Go | S_Go); LivenessAG ( N_Go N

18、_Sense AF N_Go); AG ( S_Go S_Sense AF S_Go); AG ( E_Go E_Sense AF E_Go); Fairness constraintsinfinitely often (N_Go N_Sense); infinitely often (S_Go S_Sense); infinitely often (E_Go E_Sense); All properties verified Guarantee no collisions Guarantee service assuming fairness Computational resources

19、used: 57 states searched 0.1 CPU seconds 可 以 通 过 并 行 、 抽 象 和 自 动 化 减 少 验 证 时 间并 行 ： 采 用 更 多 的 资 源 ， 设 计 实 现 与 验 证 并 行 ； 验 证编 码 与 调 试 并 行抽 象 ： 不 关 心 低 层 次 细 节 ， 事 务 级 、 总 线 周 期 级自 动 化 ： 需 要 标 准 化 的 过 程 ； 目 前 没 有 通 用 的 标 准 化方 法 ； 有 些 验 证 过 程 可 自 动 化 2/10/03 ECE 426 - Lecture 5 49 另 一 种 分 类 方 法 Black b

20、ox Verify using module I/O ports only No knowledge of implementation No access to internals White box Verify using module I/O ports and internals Full knowledge of implementation Full access to internals during simulation Gray box Verify using module I/O ports only Full knowledge of implementation N

21、o access to internals during simulation 5 验 证 的 代 价 Verification is a necessary evil. 时 间 长 ， 代 价 大 验 证 本 身 不 能 盈 利 卖 的 是 设 计 ， 而 不 是 验 证 Verification is a process that is never truly complete. Verification can only show the presence of errors,not their absence. It costs more and more to find fewer

22、and fewer errors. Question: how much is enough? 验 证 何 时 终 止 ？ Emotionally, or Intuitively; Out of money? Exhausted? Competitions product is there. Software people are happy with your hardware. There have been no bugs reported for two weeks. More rigorous criteria; All tests passed Test Plan Coverage

23、 Functional Coverage Code Coverage Bug Rates have flattened toward bottom. Part.2 Testbench Simulator 使 用 模 拟 工 具 Lint工 具 语 法 检 查 基 于 事 件 的 模 拟 工 具 基 于 周 期 的 模 拟 工 具 基 于 硬 件 原 型 的 模 拟 工 具 检 查 与 调 试 53 Linter 工 具 1/8 发 现 共 同 的 编 程 错 误 快 速 静 态 的 RTL代 码 检 查 参 数 和 功 能 调 用 间 不 匹 配 的 类 型 ， 参 数 数 目 不 匹配 在

24、执 行 程 序 前 发 现 错 误 静 态 工 具 54 int my_func(addr_ptr, ration) int *addr_ptr; float ration; return (*addr_ptr)+;main() int my_addr; my_func(my_addr); Linter 工 具 2/8:举 例 Lint输 出Src.c(3):warning:argument ration unused in function my_funcSrc.c(11):warning: my_addr may be used before set to invocation envir

25、onment 55 int my_func(addr_ptr) int *addr_ptr; return (*addr_ptr)+;main() int my_addr; my_func( return 0; Linter 工 具 3/8 56 Linter 工 具 4/8： 局 限 性只 能 发 现 特 定 类 型 的 问 题 ， 不 能 发 现 所 有 问 题只 能 发 现 代 码 结 构 方 面 的 问 题 ， 不 能 发 现 算 法 和 数 据 流的 问 题拼 写 检 查 ： 不 能 查 出 用 错 的 词过 于 严 格 ， 可 能 报 一 些 并 不 存 在 的 问 题错 误 信

26、息 的 过 滤可 以 在 写 完 代 码 后 立 即 运 行 lint工 具 57 Linter 工 具 5/8 Verilog源 代 码 的 lint Verilog更 象 汇 编 和 basic语 言 ， 无 类 型 语 言 ， 可 以 对 任意 寄 存 器 赋 任 意 值 Verilog的 linter可 以 发 现 公 共 的 问 题 。 58 Linter 工 具 6/8问 题 宽 度 不 匹 配 ， verilog 0扩 展 59 Linter 工 具 7/8 60 Linter 工 具 8/8： 实 例 部 分 硬 件 仿 真 器 与 形 式 化 验 证 工 具 ProDesig

27、n公 司 的 CHIPit Eve公 司 的 ZeBu Cadence公 司 的 Incisive Verification、 Incisive Formal Verifier 、 Xtreme III CHIPit Prodesign是 德 国 的 一 家 公 司 原 型 验 证 系 统 CHIPit Platinum Edition V4 CHIPit CHIPit Platinum Edition V4是 一 个 针 对 大 规 模 芯 片设 计 而 开 发 的 原 型 验 证 系 统 。 最 大 配 备 21个 FPGA芯 片 验 证 规 模 可 达 2000万 至 3000万 ， 系

28、 统 速 度 最 高 可 达200Mhz。 CHIPit 主 要 功 能 和 特 点 1. 适 合 大 规 模 设 计 的 架 构 多 层 板 体 系 架 构 和 3-D Switching互 连 技 术 2. 支 持 多 种 验 证 模 式 原 型 系 统 验 证 ， 模 拟 加 速 3. 便 利 的 调 试 工 具 FPGA探 针 制 作 方 便 , Readback功 能 , VCD 文 件 供波 形 浏 览 器 查 看 CHIPit4. 原 型 验 证 流 程 自 动 化 管 理5. 其 它 特 点 系 统 时 钟 可 方 便 地 通 过 软 件 进 行 配 置 ； 具 有 JTAG、

29、 PCI、 PCIX、 PCI-Express、 USB、 DVI、Ethernet等 系 统 接 口 ； 配 备 板 上 memory或 SSRAM、 SDRAM、 DDR SDRAM、 DDR2 SDRAM等 memory扩 展 子 板 ； 可 通 过 Ethernet或 者 CF卡 来 配 置 系 统 。 CHIPit 与 Hardi的 比 较 FPGA之 间 的 互 连 技 术 软 件 设 置 时 钟 频 率 和 进 行 复 位 Readback功 能 访 问 所 有 的 寄 存 器 支 持 transation验 证 模 式 集 成 了 项 目 管 理 、 综 合 、 布 线 、 延

30、 时 分 析 、 下 载 、 调 试 、 仿 真 、Co-simulation等 软 件 环 境 CHIPit和 Hardi的 互 连 接 口 相 同 ， 可 以 通 过 电 缆 连 接 CHIPit和Hardi。 CHIPit 缺 点 CHIPit的 电 压 统 一 为 3.3V， 增 加 了 子 板 设 计 难 度 和 成本 ， 引 入 了 电 平 转 换 的 延 时 。 CHIPit的 CO-Simulation功 能 是 2006年 底 才 新 增 加 的 功能 ， 缺 乏 现 成 的 Transactor， 其 CO-Simulation的 能 力 还有 待 验 证 。 CHIPit

31、无 法 对 BlockRam中 的 数 据 进 行 读 取 。 ZeBu Eve是 法 国 的 一 家 公 司 硬 件 加 速 器 方 面 的 产 品 主 要 有 Hammer和 ZeBu两 个系 列 Hammer是 基 于 处 理 器 的 硬 件 加 速 器 ZeBu是 基 于 FPGA的 硬 件 加 速 器 。 ZeBu 第 三 代 产 品 是 ZeBu-UF， 最 大 支 持 600万 门 ； 第 四 代 产 品 是 ZeBu-XXL， 最 大 支 持 1亿 门 最 新 产 品 Zebu-Server/Blade， 200M*10 ZeBu-UF ZeBu-UF是 基 于 Xilinx

32、V4LX系 列 构 建 的 一 块 PCI扩 展卡 最 大 支 持 600万 门 ， 最 高 速 度 可 达 200MHz ZeBu-UF1. 验 证 模 式 ZeBu-UF能 支 持 多 种 验 证 模 式 基 于 信 号 级 的 C/C+/SysemC 基 于 事 务 级 的 C/C+/SysemC/SystemVerilog 基 于 测 试 向 量 的 模 拟 加 速 基 于 STB的 在 线 仿 真 基 于 DirectICE的 在 线 仿 真 、 以 及 基 于 SmartICE的在 线 仿 真 ZeBu-UF2. 调 试 能 力 动 态 探 针 和 静 态 探 针 两 种 调 试

33、手 段 动 态 探 针 对 模 拟 速 度 的 影 响 较 大 对 于 在 线 仿 真 ， ZeBu还 提 供 了 类 似 逻 辑 分 析 仪 的 HW trigger来 控 制 时 钟 和 trace memory。 ZeBu-UF3. 较 丰 富 的 Transactor和 存 储 器 模 型 Transactor UART、 LCD、 PCI Express、 Ethernet、 AHB、 USB、Firewire、 JTAG等 等 SDR、 DDR、 DDR2、 DIMM SDR/DDR/DDR2、 Flash ZeBu-UF 软 件 资 源 综 合 时 需 要 调 用 Synplif

34、y， 并 有 自 己 的 编 译 工 具 对 综 合 后的 网 表 进 行 优 化 ZeBu的 编 译 器 会 自 动 对 设 计 进 行 划 分 ， 并 完 成 相 应 的 综合 、 映 射 和 布 局 布 线 ZeBu实 用 评 测 ZeBu的 加 速 性 能 易 用 性 调 试 能 力 ZeBu实 用 评 测 ZeBu-UF2， 最 大 支 持 300万 门 HOST采 用 Xeon 3G的 CPU， 内 存 4G， IDE硬 盘 。 测 试 对 象 为 L2C与 MI联 合 测 试 环 境 的 FPGA版 本 ， 外围 测 试 环 境 包 括 测 试 激 励 和 DDR2模 型 。 D

35、UT规 模 小 于 100万 门 ， 因 此 不 必 进 行 FPGA划 分 。 ZeBu实 用 评 测1. ZeBu-UF2插 入 HOST的 PCI插 槽 所 遇 到 的 问 题2. 统 一 设 计 顶 层 问 题3. IDDR与 ODDR问 题4. IDELAY问 题 5. LUT4问 题 :对 于 所 有 由 FPGA内 部 器 件 实 现 的 延 迟功 能 ， ZeBu都 不 支 持 6. DDR2模 型 问 题 ZeBu实 用 评 测测 试 结 果 0300us 300us1000usL2C与 MI运 行 在 HOST上 5m 17mL2C与 MI运 行 在 ZeBu-UF2上 2

36、.5m 12m加 速 比 50% 29% ZeBu实 用 评 测测 试 结 果CO-Simulation过 程 中动 态 探 针 对 模 拟 速 度 有 较 大 的 影 响 。加 入 动 态 探 针 的 CO-Simulation模 拟 速 度 甚 至 比 只 在HOST上 运 行 且 记 录 波 形 的 模 拟 速 度 还 要 慢 Xtreme IIICadence公 司 的 硬 件 加 速 器PalladiumXtreme两 个 系 列 Xtreme IIIXtreme III最 大 支 持 7200万 门 400kHz-800kHz板 上 存 储 器 容 量 为 18GB最 多 能 支

37、持 12个 用 户 同 时 使 用 Xtreme III1.验 证 模 式 支 持 多 种 验 证 模 式 包 括 基 于 信 号 级 的 模 拟 加 速 基 于 事 务 级 的 SystemC/C/C+/e模 拟 加 速 基 于 断 言 的 模 拟 加 速 ,不 支 持 基 于 PSL的 模 拟 加 速 ，但 Palladium III支 持 各 种 在 线 仿 真 Xtreme III2. 调 试 能 力 相 对 较 强 readmemh和 writememh查 看 和 修 改 存 储 器 单 元 ； printf（ ） 或 $display（ ） 语 句 实 时 输 出 消 息 snap

38、shot Hot-Swap功 能 Xtreme III3. 软 件 资 源 与 Cadence软 件 验 证 环 境 集 成 在 一 起 ， 能 利 用SimVision查 看 波 形 ， 进 行 事 务 和 断 言 调 试 、 具 有 软硬 件 联 合 调 试 功 能 和 覆 盖 率 统 计 功 能 4. TBA VIP 提 供 了 较 为 丰 富 的 基 于 事 务 加 速 的 验 证 IP， 包 括 PCI Express、 Ethernet、 AMBA、 AHB、 AXI等 等 与 ZeBu的 比 较1. 都 不 能 处 理 使 用 FPGA中 的 器 件 来 实 现 逻 辑 功 能2

39、. ASIC的 库 单 元 模 拟 模 型 一 般 都 会 使 用 UDP，Xtreme III能 自 动 将 UDP映 射 为 硬 件 ， 从 而 使 得 加速 ASIC库 单 元 成 为 可 能 ， 而 ZeBu不 具 备 此 功 能 3. Xtreme III支 持 通 过 层 次 方 式 直 接 访 问 位 于 加 速 器 的DUT中 的 信 号 ， 而 ZeBu不 具 备 此 功 能 与 ZeBu的 比 较4. Xtreme III能 通 过 Hot-Swap功 能 方 便 查 错 和 执 行 不能 被 加 速 的 激 励 ， 而 ZeBu不 具 备 此 功 能 。5. Xtreme

40、 III能 将 断 言 映 射 为 硬 件 ， 从 而 能 进 行 基 于断 言 的 加 速 ， 而 ZeBu不 具 备 此 功 能 。6. ZeBu-UF2支 持 STB， 但 要 求 测 试 激 励 必 须 是 可 综 合的 , Xtreme III允 许 测 试 激 励 不 一 定 都 是 可 综 合 ,也 能加 速 IFV 断 言 :监 测 设 计 中 正 确 行 为 或 错 误 行 为 的 验 证 对 象 。 断 言 将 设 计 要 求 转 换 成 了 验 证 对 象 ， 从 而 可 以 用 模拟 器 或 形 式 化 验 证 工 具 ， 评 测 设 计 要 求 是 否 被 满 足 I

41、FV 断 言 可 分 为 三 种 ， 第 一 种 为 Assertion， 用 于 描 述 设 计 所 期 望 的 正 确 行为 ； 第 二 种 为 Constraint， 用 于 描 述 设 计 所 处 环 境 的 行为 ； 第 三 种 为 Cover， 用 于 描 述 设 计 及 其 所 处 环 境 应 该会 到 达 的 状 态 。 IFV 形 式 化 验 证 的 结 果 Fail Pass Explored IFV 与 模 拟 相 比 形 式 化 验 证 不 需 要 编 写 测 试 激 励 ， 只 要 断 言 编 写 完整 ， 就 能 完 全 验 证 设 计 的 正 确 性 它 还 能

42、发 现 模 拟 所 不 容 易 查 出 的 错 误 形 式 化 验 证 的 有 效 性 依 赖 于 断 言 适 合 进 行 模 块 级 的 验 证 和 对 控 制 逻 辑 进 行 验 证 ， 否则 可 能 会 因 状 态 空 间 过 大 而 无 法 在 规 定 时 间 内 完 成验 证 。 IFV 支 持 PSL和 SVA两 种 断 言 SVA是 SystemVerilog的 断 言 ， 比 较 适 合 用 Verilog编 写 的RTL代 码 ， SVA是 免 费 的 ， 而 PSL需 要 购 买 。 SVA的 不 太 适 合 验 证 异 步 时 钟 接 口 PSL比 较 适 合 用 VHD

43、L编 写 的 RTL代 码 。 PSL的 断 言 可 以 用 于 验 证 异 步 时 钟 接 口 。 PSL的 断 言 功 能 比 SVA要 强 ， 例 如 ， PSL支 持 具 有 Liveness功 能 的 断 言 ， 但 SVA不 支 持 IFV 提 供 了 一 些 形 式 化 验 证 IP（ FVIP） 目 前 Cadence公 司 提 供 的 FVIP有 OCP2.0、 AHB和AXI IFV与 0in比 较 在 验 证 失 败 需 要 给 出 出 错 波 形 进 行 调 试 时 ， 0-IN需 要testbench通 过 模 拟 的 方 式 生 成 波 形 ， 而 IFV不 需 要

44、testbench而 快 速 生 成 波 形 。 0-IN对 VHDL的 支 持 处 于 Beta阶 段 ， 并 且 也 不 支 持 混 合 语言 ， 但 IFV完 全 支 持 VHDL， 且 也 支 持 混 合 语 言 。 Cadence在 中 国 具 有 训 练 有 素 的 形 式 化 验 证 方 面 的 工 程 师 ，而 Mentor没 有 。 IFV支 持 在 断 言 中 直 接 使 用 层 次 化 信 号 名 ， 而 0-IN不 支 持 。 Incisive Verification Cadence公 司 推 出 的 一 整 套 验 证 解 决 方 案 验 证 自 动 化 的 流 程

45、 它 的 基 础 是 Incisive Plan-to-Closure Methodology（ IPCM） Incisive Verification Plan： 即 根 据 给 出 的 设 计 要 求 制 定 可 执 行 的 验 证 计 划 、 确 定 覆 盖 标准 、 安 排 人 力 和 机 器 资 源 并 分 派 验 证 任 务 。 Execute： 根 据 验 证 计 划 建 立 验 证 环 境 、 构 建 验 证 组 件 、 自 动 生 成 测试 激 励 ， 并 进 行 软 模 拟 、 形 式 化 验 证 、 模 拟 加 速 以 及 在 线 仿 真 。 Measure： 分 析 验

46、 证 结 果 和 整 个 覆 盖 率 ， 并 与 验 证 计 划 进 行 对 照 。 React： 根 据 验 证 结 果 和 与 验 证 计 划 对 照 的 情 况 ， 修 正 设 计 和 测 试 环境 的 错 误 、 调 整 验 证 计 划 以 及 人 力 和 机 器 资 源 安 排 。 重 复 上 述 过 程 直 到 验 证 收 敛 。 Incisive Verification 为 了 提 高 测 试 程 序 的 开 发 效 率 ， IPCM强 调 测 试 激 励 的 自 动生 成 和 验 证 组 件 的 可 重 用 性 Cadence公 司 提 出 了 uRM（ Universal

47、Reuse Methodology） Cadence公 司 提 供 了 丰 富 的 已 开 发 好 的 uVC， 包 括 PCI-E、 AHB、 Ethernet、 MAC、 Datalink、 ARM、 USB、UART、 ALU等 等 。 uVC主 要 由 Driver、 Monitor和 BFM构 成 。 Driver用 于 产 生测 试 序 列 ， 并 将 之 传 递 给 BFM vBuilder :帮 助 用 户 开 发 uVC Part.4 OpenSPARC简 介 SUN UltraSPARC模 拟 与 验 证 介 绍 OpenSPARC T1/T2 代 码 环 境 硬 件 测

48、试 验 证 平 台 SIMS 体 系 结 构 级 模 拟 环 境 SAM 现 状 与 未 来 Sun 模 拟 与 验 证 Sun 的 功 能 验 证 （ 不 包 括 时 序 和 物 理 设 计 验 证 ） 处 理 器 体 系 结 构 设 计 验 证 RTL设 计 模 拟 验 证 DFT验 证 系 统 级 环 境 验 证 固 件 、 操 作 系 统 和 各 类 驱 动 使 用 工 具 软 模 拟 、 加 速 器 仿 真 、 形 式 化 验 证 商 业 工 具 +定 制 工 具 Sun 功 能 模 拟 与 验 证 流 程 处 理 器 设 计 验 证 流 程 Sun 模 拟 与 验 证 环 境 开

49、发 开 发 语 言 Verilog 继 承 /惯 性 （ T1） （ 主 要 RTL模 型 ） System Verilog （ T2 / T3） Vera （ 覆 盖 率 测 试 与 随 机 测 试 ） 模 拟 验 证 环 境 模 块 级 SAT (Stand Alone Test) 系 统 级 (全 自 动 回 归 测 试 Regression) 全 处 理 器 RTL模 型 存 储 子 系 统 系 统 级 Testbench Assertions Monitor (协 议 检 测 、 辅 助 调 试 ) Sun 验 证 的 核 心 - 仿 真 软 模 拟 速 度 限 制 ， 形 式 化

50、验 证 的 规 模 限 制 基 于 Xtrem的 Virtual Silicon 仿 真 验 证 (10,000+ VCS) 多 种 metric RTL Stablility, Bug , Coverage Sun 仿 真 验 证 原 因 系 统 级 设 计 包 括 ： 处 理 器 RTL、 存 储 子 系 统 、 系 统 组 件 和 Testbench UltraSPARC T1 系 统 级 模 型 3千 5百 万 门 （ 超 过 所 有 形 式 化 验 证 工 具 能力 ） 软 模 拟 器 一 秒 模 拟 一 个 周 期 仿 真 与 加 速 仿 真 In-Circuit 接 口 存 放

51、目 标 系 统 加 速 (高 速 模 拟 器 ) Sun同 时 使 用 了 两 种 方 式 Palladium Xtreme 以 Xtreme为 中 心 Sun 基 于 Xtreme的 仿 真 验 证 减 少 新 设 计 提 交 时 间 （ hot-swap VCS-Xsim） 简 化 、 加 速 模 型 初 始 化 (forces， PLI和 constom system tasks ) 端 模 拟 器 Xsim中 运 行 模 型 初 始 化 ， swapping到 硬 件 中 全 速 运 行 Sun 仿 真 验 证 cont. Sun基 于 Xtreme的 仿 真 验 证 （ 续 .） 快

52、 速 Check-Pointing运 行 时 保 存 snapshots (恢 复 波 形 、 调 试 ) Xtreme与 Sun定 制 模 拟 环 境 集 成 Sun定 制 的 Xtreme任 务 调 度 器 （ improve productivity） 仿 真 为 核 心 的 验 证 带 来 的 问 题 整 个 验 证 流 程 都 有 修 改 与 变 化 RTL设 计 testBench设 计 断 言 方 法 Monitor实 现 模 型 release 回 归 测 试 调 试 加 速 是 首 位 需 求 所 有 内 容 进 入 仿 真 平 台 可 综 合 设 计 ， 为 定 制 单 元

53、 开 发 可 综 合 的 简 化 RTL模 型 定 制 单 元 在 标 准 模 拟 中 无 Testbench， 要 为 仿 真 环 境 开 发 简 化 testbench Sun RTL模 拟 时 间 Sun T1 Bug报 告 Sun 模 拟 验 证 . 其 它 体 系 结 构 级 验 证 PRM Coverage （ Program Reference Manual） Directed diag, functional, traps/ASI/MMU/State-Reg Coverage Self-Checking Diag System interface Reset Verificat

54、ion Debug support Verification Microarchitecture 验 证 功 能 测 试 Unit Focused (all major block, Directed C/Perl Internal code) Memory Verification using Symbolic Simulation Clock Domain Checking Verification Performance Verification Hardware Acceleration OpenSPARC T1/T2 代 码 环 境 T1与 T2的 变 化 明 显 OpenSPARC

55、 T1/T2 代 码 环 境 激 励 代 码 量 为 RTL代 码 35倍 OpenSPARC T1/T2 代 码 环 境 Testbench代 码 量 约 是 RTL设 计 的 70% T2 SAM设 计 优 化 尚 不 包 括 perl脚 本 代 码 (SIMS Midas Goldfinger等 ) 硬 件 测 试 验 证 平 台 SIMS the Glue logic between RTL design & EDA tools 主 要 功 能 利 用 Verilog模 拟 环 境 完 成 HW设 计 模 拟T2 only VCS over SPARC 使 用 Synopsys Ver

56、a 完 成 coverage验 证 建 立 vera运 行 脚 本 和 project文 件 More： 建 立 运 行 环 境 ， 参 数 配 置 ， 控 制 其 它 工 具 Clearcase、Debussy的 配 置 与 运 行未 提 供 功 能 ： Hammer Hardware Accelerator Axis Hardware Accelerator Palladium ZeroIn sims环 境 介 绍 sims脚 本 1.272 5983行 perl脚 本 sims调 用 前 端 处 理 工 具 configsrch、 midas、goldfinger (sh+other)

57、sims/midas调 用 编 译 预 处 理 、 汇 编 和 连 接 工 具bw_cpp bw_m4 g_as g_ld gmake g_objdump等 工具 sims调 用 EDA工 具 完 成 regression sims 调 用 regreport、 vlog等 后 期 处 理 器 工 具 What sims do? 在 运 行 sims的 model目 录 下 ， 根 据 选 择 group的 不同 ， 在 cmp1/fc8子 目 录 下 根 据 diaglist选 择 激 励 和 参数 建 立 本 次 regression的 子 目 录 ， 时 间 +ID 建 立 Vera工

58、程 文 件 和 Shell 调 用 VCS编 译 Verilog代 码 （ testbench + RTL） 根 据 diaglist文 件 中 的 参 数 建 立 模 拟 命 令 为 每 一 个 测 试 建 立 子 目 录tlu_rand05_ind_03:cmp1_st:cmp1_mini_T2:0 启 动 参 数 处 理单 个 测 试 运 行 group? regression运 行退 出GetOptions: 从 命 令 行 和 配置 文 件 中 获 取 参 数是 否 rerun第 二 组 参 数 处 理diag参 数 处 理Build (vcs/vera)asm+mem.image/

59、efuse.image编 译 .vr文 件sjm和 pci的 diag JTAG/dramvcs_run/ncv_run/sim_rundiag.pl 后 期 处 理 perl代 码 流 程 逐 个 处 理 test $alias准 备 模 拟 命 令 进 入indrm(dream)call sims 单 个 test的 sims PHASE A.1 print usage title： sims第 1020行 print_header函 数 A.2 SETUP PHASE： 在 /var/temp下 建 USER:TESTBENCH目 录 A.3 preprocessing PHASE： 调

60、 用 处 理 汇 编文 件 的 Midas工 具 ， 该 工 具 是 perlmod； bw_cpp 将 diag.s转 换 为 diag.cpp； bw_m4 将diag.cpp转 换 为 diag.m4 A.4 PARSING PHASE： Midas调 用 二 进制 辅 助 工 具 goldfinger， 将 Midas的 内 容 diag.m4写 入 到 diag.midas文 件 中 ， 产 生 各 个 section的汇 编 代 码 ， 例 如 RED_SEC RED_EXT_SEC HPRIV_RESET HTRAPS TRAPS KERNEL USER_HEAP和 MAI Mi

61、das处 理 diag.midas， 解 析 其 中 的 Section， 语 法 检 查 等 。 清 除 build目 录 ， 准 备 参数 ， 调 用 ncverilog开 始 模 拟 。 单 个 test的 sims PHASE A.5 ASSEMBLY PHASE：Midas使 用 多 个 线 程 将 上 一 步 goldfinger形 成 的 汇 编 文 件 编 译成 .o模 块 文 件 ， 调 用 预 先 提 供 的 g_as二 进 制 工 具 （ g_as无 源 码 ， 但 有opensolaris可 参 照 ） A.6 LINK PHASE： Midas产 生 连 接 的 描

62、述 文 件 diag.ld_scr； 调 用 预 先 提 供 的g_ld工 具 ， 产 生 类 型 为 elf64-sparc的 diag.exe文 件 A.7 POSTPROCESSING PHASE：Midas产 生 diag.goldfinger文 件 ， Goldfinger根 据 此 文 件 产 生mem.image文 件 。 在 整 个 过 程 中 产 生 symbol.tbl， mem.image和 diag.ev三 个 文 件 。 A.8 COPY PHASE：拷 贝 文 件 ， 建 立 diag.s、 mem.imag、 diag.ev、 symbol.tbl和 diag.e

63、xe的 硬 链 接 。 A.9 CLEANUP PHASE：清 除 build目 录 ， 准 备 参 数 ， 调 用 simv开 始 模 拟 。 config args/command 按 照 group（ cmp1_mini） 参 数 选 择 sys (cmp1) 选 择 config (diag目 录下 的 diaglist子 目 录 包 含 模 拟 所 需 要 的 文 件 和 参 数 列 表 ) Diaglist文 件 T1 中 的 chip8.conf 定 义 -model cmp11 或 者 fc8 定 义 vera需 要 的 配 置 文 件 vcon cmp_top.vcon 定

64、义 模 拟 需 要 的 各 个 模 块 需 要 的 文 件 列 表 定 义 模 拟 各 个 模 块 的 配 置 -config_rtl 定 义 其 它 参 数 ， 例 如 vcs的 build参 数 -vcs_build_args 或 者 -ncv_build_args T2 diag/diaglist文 件 和 env下 filelist文 件 sims脚 本 中 使 用 opt保 存 了 具 有 177/210个 参 数 配 置 的 Hash表 Group Diag 定 义 diaglist， 默 认 的 diaglist是$DV_ROOT/verif/diag/master_diagli

65、st， 而 该 文 件 只是 引 用 了 core1.diaglist和 chip8.diaglist两 个 文 件 ， 后两 个 文 件 中 有 众 多 的 参 数 配 置 还 应 用 了 诸 如cmp2_basic.diaglist这 样 的 文 件 。 从 diaglist函 数 中 获 取 diag参 数 ， 调 用get_opt_from_diaglist(4765)函 数 。 在 该 函 数 中 将 调用 bw_cpp工 具 （ Sun的 cpp预 编 译 器 ） 来 产 生master_diaglist文 件 。 SAM环 境 OpenSPARC T1的 软 件 环 境 包 括

66、两 部 分 ： 伴 随 OpenSPARC T1项 目 一 同 开 源 的 模 拟 环 境 ， 称 为Arch.Tool； SAM-T1 SAM-2 T1/T2处 理 器 上 的 操 作 系 统 、 编 译 、 应 用 开 发 等 Sun称 为CoolTools的 相 关 软 件 。 SAM-T2的 代 码 结 构 优 于 SAM-T1， cpp代 码 减 少 ， Xml和 python代 码 增 多 思 考 的 问 题 模 拟 时 间 长 1 month (T1 cmp8/ T2 fc8) 测 试 激 励 是 否 足 够 ？ cmp1_mini 51个 激 励 FPGA原 型 和 裁 减 需 要 多 长 时 间 S1 6 months 思 考 的 问 题 确 定 整 个 芯 片 验 证 的 标 准 ？ 通 用 处 理 器 not ASIC Boot OS 典 型 应 用 (1x xx个 应 用 ) (可 行 ) Random Directed 测 试 （ Sun）