FPGA设计基础第4章设计验证(共79页)

第 四 章 设 计 验 证n 随 着 集 成 度 的 提 高 ， 系 统 的 规 模 日 益 庞 大且 复 杂 。n 强 壮 的 系 统 应 有 完 备 的 验 证 作 保 障 。n 验 证 工 作 量 远 大 于 系 统 设 计 工 作 量 。n 验 证 工 作 的 基 本 技 术 和 方 法 。 Page 1目 前 ， 验 证 一 般 通 过 仿 真 实 现本 章 节 中 ， 验 证 和 仿 真 不 加 区 分 4.1 验 证 概 述 Page 2 验 证 过 程 是 证 明 设 计 正 确 的 过 程 ， 验 证的 目 的 是 为 了 保 证 设 计 实 现 与 设 计 规 范 是 一致 的 ， 保 证 从 设 计 规 范 开 始 ， 经 过 一 系 列 变换 后 得 到 的 网 表 与 最 初 的 规 范 是 一 致 的 ， 整个 变 换 的 过 程 是 正 确 的 。4.1.1 验 证 的 概 念 Page 3 4.1 验 证 概 述1. 从 自 然 语 言 表 述 的 系 统 规 范 变 换 成 完 整 的 、 可验 证 和 无 二 义 性 的 系 统 规 范 。2. 从 系 统 规 范 变 换 成 可 实 现 的 模 块 设 计 规 范 。3. 从 模 块 设 计 规 范 变 换 成 RTL及 代 码 描 述 。4. 从 RTL代 码 通 过 综 合 工 具 变 换 成 门 级 网 表 。5. 从 门 级 网 表 通 过 后 端 布 局 布 线 工 具 变 换 成 具 有延 时 信 息 的 网 表 。 n FPGA设 计 可 能 包 含 的 几 个 变 换 ： Page 4 4.1 验 证 概 述验 证 是 一 个 多 次 重 复 的 过 程 ， 是 一 个 不 断 向 期望 结 果 靠 近 的 过 程 。系 统 规 范 网 表交 换验 证 Page 5 4.1 验 证 概 述n 验 证 和 测 试 是 ASIC设 计 流 程 中 两 个 不 同 的 环 节 。 u 验 证 的 目 的 则 是 为 了 确 认 设 计 符 合 设 计 规 范 ，目 前 验 证 一 般 通 过 仿 真 实 现 。u 测 试 的 目 的 是 为 了 确 认 生 产 后 的 设 计 产 品 是否 合 格 、 正 确 ， 一 般 由 加 工 厂 家 或 封 装 测 试厂 家 完 成 。4.1.2 验 证 和 测 试 （ Verification vs Test） 4.1 验 证 概 述系 统 规 范 网 表 芯 片电 路 设 计 生 产验 证 （ 仿 真 ） 测 试 对 物 理 器 件 高 低 电 平 的 确 认不 属 于 本 教 材 范 畴对 设 计 规 范 及 功 能 的 确 认 Page 6 4.1 验 证 概 述n 传 统 的 电 子 线 路 设 计 验 证 方 法4.1.3 Top-Down/Bottom-Up 验 证 方 法n 目 前 的 电 子 线 路 设 计 验 证 方 法逻 辑 设 计 、 画 电 路 图 、 搭 建 电 路 、 测 试 验 证借 助 EDA 工 具 在 计 算 机 上 进 行 RTL 级 设计 和 验 证 。 Page 7 4.1.3 Top-Down/Bottom-Up 验 证 方 法n Top-Down 验 证 法1. 系 统 级 验 证 ： 根 据 系 统 规 范 对 系 统 进 行 建 模 ，并 对 建 立 的 模 型 进 行 验 证 。2. 功 能 验 证 ： 验 证 设 计 的 RTL代 码 应 符 合 系 统 规范 。 主 要 方 法 -功 能 仿 真 (形 式 化 验 证 为 辅 )。3. 门 级 网 表 验 证 ： 通 过 功 能 仿 真 或 形 式 化 工 具检 验 RTL代 码 和 综 合 后 网 表 的 是 否 相 等 。4. 时 序 验 证 ： 验 证 综 合 后 含 有 延 时 信 息 的 网 表 时序 是 否 满 足 要 求 。 对 于 同 步 设 计 一 般 通 过 静 态时 序 分 析 工 具 完 成 验 证 。 Page 8 4.1.3 Top-Down/Bottom-Up 验 证 方 法n Bottom-Up 验 证 法1. 模 块 级 验 证 -验 证 模 块 的 各 种 工 作 情 况 ， 保证 每 个 单 元 的 设 计 质 量 。2. 子 系 统 验 证 、 系 统 级 验 证 -分 层 次 组 装 模 块进 行 子 系 统 验 证 直 至 完 成 系 统 级 验 证 。备 注 ： 系 统 级 验 证 ， 目 标 是 验 证 整 个 设 计 的 功 能 。 验证 主 要 集 中 在 设 计 和 外 环 境 之 间 能 否 协 调 工 作 ， 包括 一 些 极 端 情 况 、 边 界 条 件 和 错 误 处 理 等 。 Page 9 n 目 前 主 流 的 两 类 “ 验 证 技 术 ” ：4.1.4 验 证 技 术（ 1） 基 于 形 式 化 的 验 证 -通 过 数 学 的 方 法 ， 证 明设 计 的 功 能 是 否 与 规 范 一 致 。u 等 价 性 检 验 ： 比 较 两 个 设 计 是 否 完 全 等 价 。 两 个 网 表 比 较 ， 网 表 与 RTL代 码 比 较 u 模 型 检 验 ： 根 据 设 计 的 RTL代 码 ， 提 取 有 限 状 态 机 并 穷 举搜 索 设 计 状 态 空 间 ， 验 证 设 计 特 性 。 模 型 检 验 工 具 ： Cadence的 FormalCheck、 IBM的 Sugar和 Sypopsys的 Veran 局 限 性 很 大1、 设 计 规 模 越 来 越 大 复 杂2、 模 型 检 验 所 描 述 的 特 性有 限 4.1.4 验 证 技 术（ 2） 基 于 TestBench的 验 证 (目 前 主 要 的验 证 方 式 ) Testbench测 试 平 台 即 ： Testbench产 生 激 励 给 被 验 证 设 计（ DUV） 或 待 测 设 计 （ DUT） ， 同 时检 查 DUV/DUT输 出 是 否 满 足 要 求 Page 10 4.1.4 验 证 技 术n TB 结 构 模 型 1. 黑 盒 验 证 法 2. 白 盒 验 证 法3. 灰 盒 验 证 法解 释 ：DUV/DUT Design Under VerificationDesign Under Test Testbench功 能 ：n 为 DUV/DUT提 供 激 励 信 号n 正 确 实 例 化 DUV/DUTn 将 仿 真 数 据 显 示 在 终 端 或 者 存 为 文 件 ，也 可 以 显 示 在 波 形 窗 口 用 于 分 析 n 复 杂 设 计 可 以 使 用 EDA工 具 ， 自 动 比 较仿 真 结 果 与 理 想 值 。激 励 实 例 化DUT 终 端 显 示 值 、 存 成 文 件波 形 显 示自 动 比 较 结 果 正 确 性 4.1.5 仿 真 工 具1、 仿 真 器仿 真 器 是 验 证 中 最 常 用 的 工 具 。 仿 真器 试 图 创 建 一 个 能 够 模 拟 真 实 设 计 的 工 作环 境 ， 使 验 证 工 程 师 和 设 计 进 行 交 互 ， 在设 计 生 产 之 前 发 现 设 计 错 误 ， 以 减 少 损 失 。之 所 以 称 为 仿 真 器 ， 是 因 为 它 们 是 真 实 状态 的 一 种 近 似 。 Page 11 Page 12 4.1.5 仿 真 工 具验 证 人 员 在 仿 真 器 中 ， 通 过 testbench 为 设 计 提 供 输 入 激 励 (为 电 路 建 立 模 拟 工 作环 境 )， 仿 真 器 通 过 一 定 方 式 与 验 证 人 员 交互 ， 将 电 路 的 输 出 状 态 随 环 境 变 化 的 信 息 反映 给 验 证 人 员 。业 界 常 用 的 仿 真 器 有 ： Cadence 的 NC-Verilog, Synopsys的 VCS 和 Mentor的ModelSim Page 13 4.1.5 仿 真 工 具最 常 见 的 和 仿 真 器 一 起 使 用 的 验 证 工 具 。 通过 波 形 观 察 器 的 图 形 界 面 ， 设 计 人 员 可 以 直 观 地观 察 随 时 间 变 化 的 信 号 以 及 信 号 之 间 的 相 互 关 系 ，定 位 设 计 错 误 或 测 试 文 件 的 错 误 。2、 波 形 观 察 器 工 具TB运 行 中 即 统 计 被 测 设 计 代 码 的 测 试 覆 盖 情况 ， 给 出 报 告 ， 验 证 者 可 依 据 此 报 告 分 析 判 断 验证 工 作 的 完 备 性 。 几 个 主 要 覆 盖 分 析 方 面 ：3、 代 码 覆 盖 分 析 工 具 4.1.5 仿 真 工 具使 用 代 码 覆 盖 技 术 必 须 非 常 了 解 设 计 细节 ， 通 过 代 码 覆 盖 分 析 工 具 了 解 哪 些 语 句 、路 径 已 经 被 执 行 ， 那 些 表 达 式 已 经 被 执 行 ，那 些 过 程 没 有 被 触 发 等 等 ， 然 后 修 改 测 试 程序 ， 提 高 代 码 覆 盖 率 。 提 高 覆 盖 率 可 以 提 高 测 试 的 完 备 性 。n 语 句 覆 盖n 路 径 覆 盖n 表 达 式 覆 盖 n 触 发 覆 盖n 自 动 机 覆 盖 Page 15 4.1.6 验 证 计 划 和 流 程随 着 设 计 规 模 的 加 大 ， 验 证 工 作 量 越 来越 大 ， 制 定 验 证 计 划 或 者 验 证 规 范 是验 证 过 程 的 一 个 重 要 环 节 ， 验 证 计 划 可 以提 高 验 证 效 率 ， 减 少 验 证 的 盲 目 性 。制 定 验 证 规 范 在 系 统 设 计 规 范 签 收 (signoff) 后 开 始 。 Page 16 4.1.6 验 证 计 划 和 流 程应 该 注 意 ：n 验 证 工 程 师 应 与 总 体 设 计 师 以 及 设 计 人 员 一起 讨 论 整 个 设 计 功 能 、 模 块 划 分 、 接 口 方 式等 ， 详 尽 理 解 设 计 规 范 。n 在 此 基 础 上 制 定 验 证 方 案 -确 定 需 要验 证 的 功 能 特 性 ， 确 定 验 证 策 略 ， 规 划 验 证环 境 和 验 证 程 序 的 开 发 ， 确 定 整 个 验 证 所 需的 验 证 人 员 的 数 目 ， 资 源 和 时 间 等 等 。 Page 17 4.1.6 验 证 计 划 和 流 程 n 典型的验证流程 Page 18 4.1.6 验 证 计 划 和 流 程n 验 证 方 案 的 要 点 （ 验 证 什 么 、 如 何 验 证 ）1. 确 定 设 计 需 要 验 证 的 特 性 （ 验 证 内 容 ） ；2. 确 定 验 证 策 略 -系 统 级 /模 块 级 ， 黑 /白 /灰 盒 式验 证 ， 激 励 产 生 策 略 ， 验 证 响 应 方 式 （ 观 察 法 、记 录 法 、 自 检 查 法 ） ， 人 员 、 设 备 、 环 境 管 理安 排 等 。3. 确 定 验 证 方 法 -具 体 验 证 的 步 骤 和 方 法 ， 如 自顶 向 下 /自 下 向 上 ， 激 励 的 具 体 方 式 等 。 4.1.6 验 证 计 划 和 流 程4. 制 作 标 准 的 测 试 组 件 和 测 试 模 板 。5. 个 人 编 制 相 关 部 分 的 测 试 方 案 ；6. 编 制 、 调 试 测 试 程 序 ， 进 行 系 统 测 试 。7. 测 试 记 录 及 分 析 ， 编 制 测 试 报 告 。n 回 归 测 试 ： 对 发 现 问 题 修 改 后 的 设 计 重新 测 试 。 （ 1） 确 认 修 改 是 否 正 确 （ 2） 修 改 是 否 影 响 其 他 设 计 4.2 功 能 验 证所 谓 的 “ 验 证 程 序 ” - 是 对 “ 待 测 电 路 ” 的 输 入 序 列 和 预 期 输 出 相 应 的 代 码 集 合 。4.2.1 验 证 程 序 (TestBench)的 组 成 Testbench 被验证设计DUV 参考模型 输出响应输入激励 比较结果一 个 典 型 的 验 证 程 序 模 型 4.2.1 验 证 程 序 (TestBench)的 组 成一 个 典 型 的 Testbench的 六 个 组 成 部 分 ：1. DUV (被 验 证 的 设 计 )- Design Under Verification，可 能 是 RTL设 计 ， 也 可 以 是 网 表 。2. 输 入 激 励 - 产 生 DUV需 要 的 各 种 输 入 信 号 。3. 时 序 控 制 模 块 - 产 生 TB和 DUV所 需 的 时 钟 信 号 。4. 参 考 模 块 - 产 生 预 期 信 号 （ 行 为 级 编 码 模 块 /以 验证 过 正 确 的 设 计 ） 。5. 诊 断 记 录 - 相 关 信 号 变 化 情 况 的 记 录 。 6. 断 言 检 查 器 - 对 特 定 的 信 号 形 式 检 测 。 编 写 仿 真 激 励 ：n 1、 仿 真 激 励 与 被 测 对 象 的 连 接模 块 实 例 的 端 口 方 式 ：（ 1） 名 称 对 应 ： 将 模 块 实 例 外 部 的 信 号 直 接 对 应 于 模 块 的 端 口 名 称 。module halfadd(x,y,sum,cout);endmodule名 称 对 应halfadd u_halfadd_a(.x(ax),.y(ay),.sum(asum),.cout(acout);（ 2） 位 置 对 应 ： 外 部 信 号 按 照 该 模 块 端 口 声 明 的 顺 序 一 一 对 应 。Halfadd u_halfadd_b(bx,by,bsum,bcout); n 2、 使 用 initial语 句 和 always语 句 通 常 主 动 产 生 激 励 用 initial， 被 动 检 测 响 应 用 always。 前者 执 行 一 次 ， 后 者 不 断 重 复 执 行 。 在 initial中 多 次 运 行 一个 语 句 块 ， 使 用 嵌 入 循 环 语 句 ： while、 repeat、 for和forever。initialbegin forever bengin . endend 条 件 发 生 时 执 行always (posedge clk)begin siga=sigb end n 3、 时 钟 、 复 位 写 法（ 1） 普 通 时 钟 信 号 /产 生 一 个 周 期 为 10的 时 钟 parameter FAST_PERIOD=10; reg clk; initial begin clk=0; forever #(FAST_PERIOD/2) clk=clk; end 用 always产 生 一 个 周 期 为 10的 时 钟 parameter FAST_PERIOD=10; reg clk; initial clk=0; always #(FAST_PERIOD/2) clk=clk; （ 2） 非 50%占 空 比 时 钟 parameter Hi_time=5; parameter Lo_time=10; reg clk; always begin #Hi_time clk=0; #Lo_time clk=1; end由 于 clk0时 刻 未 初 始 化 ， 前 5纳 秒 输 出 为 x （ 3） 固 定 数 目 时 钟产 生 两 个 高 脉 冲 parameter PulseCount=4， PERIOD=10; reg clk; initial begin clk=0; repeat (PulseCount) #(PERIOD/2) clk=clk; end (4)异 步 复 位 信 号 parameter PERIOD=10; reg Rst_n; initial begin Rst_n=1; #PERIOD Rst_n=0; #（ 5*PERIOD） Rst_n=1; end Rst_n为 低 有 效 ， 代 码 表 示 10ns时 复 位 ， 复 位 延 时 50ns （ 5） 同 步 复 位 ： initial begin Rst_n=1; （ negedge clk); /等 待 时 钟 下 降 沿 Rst_n=0; #30； （ negedge clk); /等 待 时 钟 下 降 沿 Rst_n=1; end 另 一 种 同 步 复 位initial begin Rst_n=1; （ negedge clk); /等 待 时 钟 下 降 沿 Rst_n=0; /复 位 开 始 repeat （ 3） （ negedge clk); /经 过 3个 时 钟 下 降 沿 Rst_n=1; /复 位 撤 销 end 4、 利 用 系 统 函 数 和 系 统 任 务 display在 显 示 数 据 $display(“Addr:%b-Data:%d”,add,data); 时 序 检 查 系 统 任 务 $setup(sig_d,posedge clk,1);/若 clk上 升 沿 到达 之 前 的 1ns时 间 内 sig_d发 生 跳 变 ， 则 建 立 时间 不 足 告 警 $hold(posedge clk, sig_d,0.1);/若 clk上 升 沿 到达 之 后 的 0.1ns时 间 内 sig_d发 生 跳 变 ， 则 保 持时 间 不 足 告 警 dato_out=$random%256;从 文 本 文 件 中 读 出 和 写 入 数 据 （ 类 似 C语 言 文 件 操 作 ） 搭 建 仿 真 环 境 单 顶 层 的 TestBench代 码 ： module testbench;/测 试 平 台 顶 层/时 钟 激 励 产 生 initial bengin end/复 位 激 励 产 生 initial begin end /各 种 测 试 激 励 initial bengin end /设 计 模 块 实 例mpi u_mpi (.clk (clk),.rst_n(rst_n),.mpi_data(data),.mpi_addr(addr),.mpi_csn(csn),.mpi_rw(rw); 确 认 仿 真 结 果1、 直 接 观 测 波 形2、 观 察 文 本 输 出 利 用 系 统 任 务 打 印 的 信 息 查 看 仿 真 结 果 ，$display、 $monitor、 $fdisplay3自 动 检 查 仿 真 结 果（ 1） 数 据 库 比 较 法 。 （ 数 据 库 存 储 期 望 结 果 ）（ 2） 波 形 比 较 法 。 （ 存 储 标 准 波 形 ， 仿 真 结 果 与 其 比 较 ）（ 3） 动 态 自 检 法 。 编 写 行 为 级 与 DUT功 能 一 致代 码 ， 同 时 读 入 激 励 ， 比 较 输 出 结 果 举 例 ： 加 法 器 Page 22 4.2.1 验 证 程 序 (TestBench)的 组 成Book Page141 例 ： 一 个 编 码 器 的 验 证 。 Page 23 4.2.2 实 用 构 造 Testbench技 术1、 使 用 代 码 描 述 验 证 模 型 编 写 的 电 路 模 型 代 码 ， 要 从 实 现的 角 度 出 发 ， 从 物 理 实 现 上 考 虑 verilog代 码 的 写法 ， 写 出 的 代 码 必 须 是 可 综 合 的 。编 写 的 用 于 验 证 的 代 码 不 必 考 虑到 内 部 的 实 现 问 题 ， 只 要 按 规 范 描 述 出 一 个 设 计的 功 能 就 可 以 了 ， 也 就 是 说 只 要 建 立 一 个 设 计“ 逻 辑 模 型 ” 。行 为 模 型 代 码 的 描 述 往 往 比 RTL代 码 的 描 述 简单 的 多 ， 容 易 正 确 描 述 电 路 功 能 。 Page 24 4.2.2 实 用 构 造 Testbench技 术2、 使 用 行 为 级 代 码 可 以 不 受 可 综 合 要 求 的 约 束 ， 可 以在 更 高 的 层 次 上 实 现 数 据 的 抽 象 ， 使 得 验 证 程 序 编写 时 更 方 便 。 数 据 类 型 -数 字 滤 波 器 的 仿 真 例 子 (P148； 例 4.4)。 数 据 类 型 -记 录 是 一 种 抽 象 的 数 据 结 构 ，可 以 由 不 同 类 型 信 息 组 成 ， 可 以 方 便 的 表 示 在 具有 一 定 结 构 的 数 据 。 Verilog语 言 本 身 并 不 支 持 记录 结 构 ， 通 过 一 些 方 法 可 以 模 拟 记 录 的 实 现 。 Page 25 n 记 录 的 用 法n 记 录 的 用 途在 仿 真 中 主 要 用 于 描 述 一 定 格 式 的 数 据 块 。创 建 一 个 没 有 参 数 的 module， 内 部 的 所 有 变 量都 用 寄 存 器 类 型 声 明 。 当 模 块 实 例 化 后 ， 用 模 块中 定 义 的 变 量 表 示 记 录 中 的 域 。对 记 录 可 以 进 行 行 为 级 的 处 理 ， 准 备 好 仿 真 数据 。 4.2.2 实 用 构 造 Testbench技 术 Page 30 4.2.2 实 用 构 造 Testbench技 术 多 维 数 据 类 型 -数 组 类 型 是 记 录 类 型的 特 例 （ 域 等 长 ， 二 维 数 组 在 设 计 中 也 用 于对 RAM 等 数 据 结 构 的 建 模 ） 。 测 试 激 励 需 要构 造 有 固 定 格 式 的 数 据 帧 时 ， 使 用 二 维 数 组是 一 种 较 好 的 方 法 。 （ 例 如 SDH 数 据 帧 信 元 的 构 成 等 ） Page 31 4.2.2 实 用 构 造 Testbench技 术3、 编 写 的 仿 真 代 码 行 为 代 码 通 常 按 功 能 和 需 求 划 分 结 构 ， 复 杂 的仿 真 功 能 ， 可 以 按 功 能 划 分 若 干 个 子 功 能 ， 然 后 编写 行 为 代 码 实 现 这 些 子 功 能 。 在 Verilog中 ， 可 以 用module， function 和 task 实 现 仿 真 代 码 结 构 化 。是 实 现 结 构 化 仿 真 编 码 的 主 要 手 段 ， 封 装的 主 要 思 想 是 将 实 现 的 细 节 隐 藏 起 来 ， 将 功 能 和 它的 实 现 完 全 分 离 开 ， 只 要 封 装 的 接 口 不 变 ， 实 现 的修 改 和 优 化 不 影 响 用 户 的 使 用 。 Page 32 4.2.2 实 用 构 造 Testbench技 术n 实 现 封 装 的 几 种 方 法 变 量 局 部 化 方 法 一 : 变 量 声 明 时 局 部 化尽 可 能 地 将 变 量 的 声 明 局 部 化 ， 避 免 变 量在 其 它 模 块 间 相 互 作 用 ， 产 生 不 正 确 地 结 果 。 方 法 二 : 用 task 和 function 使 变 量 局 部 化 在 verilog语 言 中 ， 用 task 和 function 也 可以 使 说 明 局 部 化 。 Page 33 4.2.2 实 用 构 造 Testbench技 术integer I; / 全 局 I.always begin for (I = 0; I0, I = I - 1) begin end end always begin ： block_1 integer I; /局 部 I for (I=0; I0, I=I-1) begin end end Page 34 4.2.2 实 用 构 造 Testbench技 术n 实 现 封 装 的 几 种 方 法 总 线 功 能 模 型 (Bus Function Module) 总 线 功 能 模 型 BFM， 也 称 为 事 务 处 理 程 序（ transactions） 描 述 模 块 。 所 谓 BFM就 是 DUV和 TB之 间 的 一 种 抽 象 ， 它 是 任 务 的 集 合 ， 集 合中 的 每 个 任 务 完 成 一 个 特 定 的 事 务 ， 事 务 可 以是 非 常 简 单 的 操 作 ， 如 内 存 的 一 次 读 、 写 ， 也可 以 是 非 常 复 杂 的 操 作 ， 如 通 信 中 结 构 化 的 数据 包 。 BFM被 直 接 链 接 到 DUV上 ， TB通 过 “ 函数 /功 能 ” 调 用 实 现 DUV的 操 作 。 Page 35 4.2.2 实 用 构 造 Testbench技 术TB-BFM-DUV 模 型 Page 36 例 4.11 带 有 微 机 接 口 芯 片 MPI 的 仿 真 。CPU接 口 可 抽 象 成 右 图形 式 。 根 据 预 定 义 的 协 议 ，由 CPU BFM产 生 CPU接 口所 需 要 的 实 际（ 图 右 侧 信 号 ） ， 图 左 侧接 口 用 特 定 的 数 据 初 始 化一 个 事 务 ， 根 据 不 同 的 事务 ， CPU BFM产 生 不 同 物理 信 号 ， 把 左 侧 的 接 口 称为 。 在 BFM中 根 据 CPU接 口 的 时 序 ， 应 用 task产 生 一 次CPU读 写 操 作 所 需 要 的 各 种 信 号 。 Page 37 module （ A, D, ALE, WRB, RDB, CSB); output 13:0 A; /地 址 总 线 inout 7:0 D; /双 向 数 据 总 线 output ALE, WRB, RDB, CSB; /控 制 线 reg 13:0 A; reg ALE, WRB, RDB, CSB; / 定 义 CPU读 写 信 号 的 所 需 要 的 时 序 参 数 parameter tSalr = 10, tSlr = 5, Prd = 30, tHrd = 10;parameter tHar = 10, tVl = 5, tSalw = 10, tVwr = 40, parameter tSdw = 20, tSlr = 5；parameter data_width = 8, addr_width = 14;reg data_width - 1 :0 work_reg; Page 38 task rd_cpu; /读 操 作 的 时 序 ； input addr_width - 1:0 addr; begin #10 A = addr; CSB = 1b0; #(tSalr-tVl) ALE= 1b1; #tVl ALE=1B0; #tSlr RDB = 1B0; #Prd work_reg = D; RDB = 1B1; #tHar A = 14hzzzz; CSB = 1b1; end endtask task wr_cpu ; /写 CPU操 作 input addr_width:0 addr; input data_width:0 write_value; begin #10 A = addr; CSB = 1B0; #(tSalw-tVl) ALE = 1B1; #tVl ALE = 1B0; #tSlw WRB = 1B0; #(tVwr-tSdw) D = write_value; WRB = 1b1; #tHdw Release D; A = 14Hzzzz; CSB = 1B0; endendtaskendmodule /cpu_interface Page 39 在 测 试 程 序 中 ，实 例 化 cpu_bfm模块 ， 直 接 和 被 测 试的 设 计 连 接 ， 通 过层 次 关 系 调 用 元 件的 cpu任 务 ， 实 现对 目 标 器 件 的 读 写操 作 。 module testbench； . cpu_inst (.A(A), .D(D), .ALE(ALE), .WRB(WRB), .RDB(RDB), .CSB(CSB); DUV DUV_inst ( /* other signal */ /* cpu signal */ .A(A), .D(D), .ALE(ALE), .WRB(WRB), .RDB(RDB), .CSB(CSB), /* other signal */ . );例 4.12 cpu_interface 的 使 用 方 法 Page 40 initial begin #300 cpu_inst.rd_cpu(14h 0010); / 此 时 cpu_inst. work_reg 中 既 存 储 了 读 出 的 数 ; /other operation #1000 cpu_inst.wr_cpu(14h 0001, 8h3C); ; /other operation endendmodule / testbench例 4.12 的 使 用 方 法 Page 41 4、 编 写 具 有 的 仿 真 代 码 4.2.2 实 用 构 造 Testbench技 术上 面 的 CPU接 口 的 仿 真 代 码 例 子 中 包 含 了 一 定的 层 次 结 构 。 验 证 工 程 师 在 最 顶 层 ， 只 需 要 写 出 特定 的 完 成 某 项 功 能 验 证 的 事 务 序 列 ， 而 这 些 序 列 中的 事 务 去 调 用 不 同 的 事 务 处 理 程 序 ， 这 些 不 同 的 事务 处 理 程 序 又 可 以 去 调 用 更 低 层 的 事 务 处 理 程 序 ，以 产 生 CPU接 口 所 需 要 的 物 理 信 号 。 这 种 层 次 化 结构 ， 可 以 为 验 证 工 程 师 提 供 一 个 良 好 的 可 操 作 环 境 ，使 他 们 更 关 注 于 DUV的 验 证 而 不 是 注 意 如 何 产 生DUV接 口 信 号 。 Page 42 5、 编 写 具 有 自 检 查 功 能 的 仿 真 程 序 4.2.2 实 用 构 造 Testbench技 术设 计 的 有 效 性 必 须 通 过 设 计 对 激 励 响 应 的 结 果 得以 体 现 ， 有 可 以 设 计 响 应 。 通 过 人 工 观 测 DUV输 出 波 形 的 结 果 是 否 正 确 ； 通 过 日 志 的 方 式 ， 将 一 些 结 果 输 出 到 文 件 中 ，在 仿 真 结 束 后 ， 分 析 日 志 文 件 ； 自 检 查 方 式 ； Page 43 6、 验 证 代 码 的 重 用4.2.2 实 用 构 造 Testbench技 术大 规 模 FPGA/ASIC设 计 一 般 由 多 个 层 次 构 成 ，设 计 人 员 应 对 各 个 层 次 上 的 子 模 块 逐 一 验 证 ，然 后 将 这 些 验 证 过 的 模 块 连 接 在 一 起 形 成 高 层规 模 较 大 的 设 计 。 为 这 些 不 同 的 子 模 块 开 发 不同 的 验 证 环 境 需 要 花 费 大 量 的 时 间 和 精 力 ， 验证 重 用 是 解 决 这 一 问 题 的 有 效 方 法 ， 验 证 人 员利 用 大 量 的 可 重 用 验 证 模 块 构 造 出 不 同 层 次 模块 的 验 证 环 境 。 Page 44 6、 验 证 代 码 的 重 用 -两 种 形 式4.2.2 实 用 构 造 Testbench技 术 同 一 个 芯 片 设 计 中 验 证 重 用 在 验 证 的 不 同 周 期 或 设 计 的 不 同 阶 段 验 证 代 码 的 重 用 。好 的 验 证 代 码 可 以 在 和 验 证 时 均 可 重 用 。 不 同 芯 片 设 计 之 间 的 重 用 验 证 代 码 可 以 用 于 同 一 芯 片 的 更 新 换 代 上 ， 或 用 于 一个 包 含 许 多 标 准 设 计 模 块 的 芯 片 或 与 以 前 设 计 有 相 同 性的 新 设 计 中 。 Page 45 6、 验 证 代 码 的 重 用4.2.2 实 用 构 造 Testbench技 术重 用 的 模 块 越 多 ， 所 考 虑 的 事 项 和 投 入 的 精 力 就 越 多 。需 要 在 验 证 重 用 所 取 得 的 效 果 和 投 入 重 用 的 资 源 做 些 平衡 。 专 用 的 测 试 代 码VIP DUV VIP 可 重 用 的 验 证 元 件仿 真 程 序 被 划 分 成 两 个 主 要 的 部 分 ： 可 重 用 的 验 证代 码 与 专 用 的 验 证 代 码 。 Page 46 4.3 基 于 断 言 的 验 证基 于 断 言 的 验 证 是 一 种 有 效 的 “ 白 盒 ” 验 证 方 法 ，它 在 RTL设 计 的 源 代 码 中 监 视 系 统 的 关 键 行 为 ， 特 别 是 在某 些 特 殊 情 况 下 的 行 为 。 通 过 断 言 的 方 法 ， 可 以 增 加 观测 点 ， 在 仿 真 过 程 中 及 时 发 现 设 计 错 误 。 断 言 中 用 到 的 概 念 ： 特 性 （ Property） : 用 于 刻 画 设 计 特 征 的 一 些 行 为 属 性 。 事 件 （ Event） : 验 证 过 程 的 一 个 行 为 。 断 言 （ Assertion） : 用 于 监 控 或 检 查 施 加 在 设 计 上 的 一 些规 则 和 假 设 的 一 种 机 制 。 Page 47 4.3 基 于 断 言 的 验 证用 户 可 以 用 各 种 硬 件 描 述 语 言 如 Verilog、 VHDL 或System C 等 形 成 断 言 以 监 视 设 计 在 仿 真 过 程 中 的 行 为 。也 可 以 利 用 已 有 的 断 言 库 ， 将 断 言 直 接 加 入 到 设 计 中 。 如 ：Accellera（ ） 推 出 的 采 用 了 断 言 思 想的 验 证 库 （ Open Verification Library） ， 该 库 中 用HDL语 言 （ VHDL和 Verilog） ， 定 义 和 实 现 了 一 些 非 常 常用 的 属 性 声 明 。一 些 专 用 的 硬 件 特 性 描 述 语 言 （ Property Specification Language: ） 和 断 言 语 言 已 经 称 为 工 业 标 准 ， 并 开 始推 向 市 场 ， 例 如 IBM公 司 开 发 的 语 言 已 被 Accellera组 织 接 受 ， 成 为 PSL工 业 的 标 准 。 Page 48 4.3 基 于 断 言 的 验 证断 言 可 以 有 多 种 实 现 方 法 ， 最 常 用 、 最 简 单 的 方 法 是 所谓 的 “ 叙 述 性 ” 的 实 现 方 法 ， 即 在 设 计 结 构 中 描 述 断 言 ，断 言 和 设 计 中 的 其 他 结 构 一 起 并 发 地 计 算 。叙 述 性 断 言 实 际 上 是 一 些 代 码 ， 这 些 代 码 中 一 般 包 含 三部 分 ： 断 言 的 条 件 ， 报 告 信 息 ， 错 误 的 严 重 程 度 以及 相 关 的 处 理 。 例 ： assert_always #(severity_level, options, msg) inst_name (clk, reset_n, test_expr) 备 注 ： assert_always模 块 是 Accellera组 织 OVL库 中 的 标准 件 ， 详 见 书 中 page166 。 Page 49 module counter_0_to_9(reset_n,clk); define ASSERT_ON 1 input reset_n, clk; reg 3:0 count; always (posedge clk) begin if (reset_n = 0 | count = 9) count = 1b0; else count = count + 1; end assert_always #(0, 0, error: count not within 0 and 9) valid_count (clk, reset_n, (count = 4b0000) /always断 言endmodule 例 4.14 模 9计 数 器 中 使 用 always断 言 。 Page 50 4.3 基 于 断 言 的 验 证一 个 断 言 实 际 上 就 是 一 段 Verilog代 码 ， 用 模 块 的 形 式将 其 封 装 起 来 。 使 用 时 直 接 实 例 化 ， 把 断 言 嵌 入 在 设 计 中 ，当 测 试 条 件 不 成 立 的 时 候 ， 触 发 该 断 言 。 在 验 证 中 使 用 断 言 的 优 点 ：n 节 约 仿 真 时 间 ， 一 旦 出 现 了 仿 真 错 误 ， 可 以 立 即停 止 仿 真 ； n 增 加 了 设 计 的 可 观 察 性 ；n 减 少 设 计 错 误 定 位 时 间 ， 可 以 准 确 而 快 速 定 位 设计 错 误 ；n 减 少 人 为 干 预 ， 自 动 监 控 测 试 。 Page 51 4.4 时 序 验 证时 序 验 证 的 目 的 是 为 了 确 认 物 理 实 现 的 电 路 时 序 是 否满 足 时 序 规 范 要 求 。 时 序 验 证 的 方 法 分 为 动 态 验 证 和 静 态验 证 两 种 ， 本 节 简 单 地 介 绍 静 态 时 序 分 析 中 的 一 些 基 本 概念 。 （ 备 注 ： 简 介 动 态 时 序 分 析 概 念 。 ）4.4.1 静 态 时 序 分 析 概 述 静 态 时 序 分 析 是 通 过 分 析 设 计 中 所 有 可 能 的 信 号 路 径以 确 定 时 序 约 束 是 否 满 足 时 序 规 范 ， 不 依 赖 于 激 励 ， 且可 以 穷 尽 所 有 路 径 ， 运 行 速 度 快 ， 占 用 内 存 少 。 对 于 同步 设 计 电 路 ， 仅 借 助 于 静 态 时 序 分 析 工 具 即 可 完 成 时 序验 证 的 任 务 。 Page 52 4.4 时 序 验 证n 常 见 的 静 态 时 序 分 析 的 工 具Synopsys公 司 的 Primetime和 Mentor Graphic 公 司 的 SST Velocity是 比 较 有 影 响的 用 于 全 定 制 IC时 序 分 析 的 工 具 。 FPGA供 应 商 如 Altera， Xilinx和 Actel也 在 其 集 成环 境 中 嵌 入 了 静 态 时 序 分 析 工 具 。 Page 53 n 四 种 基 本 时 序 路 径 ： 路 径 1(Path1)： 从 输 入 管 脚到 D触 发 器 的 输 入 ；路 径 2(Path2)： 从 D触 发 器 的输 入 到 下 一 个 D出 发 器 的输 入 ； 路 径 3(Path3)： 从 D触 发 器 的输 入 到 输 出 管 脚 ；路 径 4(Path4)： 从 输 入 到 输 出 ；时 钟 路 径 （ clock path） ： 从 一 个 时 钟 的 输 入 通 过 一 个 或 多 个 缓 冲 器 到 达 一 个 时 序 元 件 的 时 钟 管 脚 的 路 径 ； Page 54 4.4.1静 态 时 序 分 析 概 述一 条 路 径 的 延 时 等 于 在 该 条 路 径 上 所 有 元 件 延 时 和 连 线 延 时之 和 。 静 态 分 析 工 具 通 过 反 向 跟 踪 路 径 终 点 到 起 点 所 有 的 延 时来 计 算 路 径 的 传 输 延 时 。在 时 序 分 析 中 ， 禁 止 组 合 环 的 存 在 ， 要 求 所 有 的 反 馈 路 径 都可 以 在 时 钟 边 界 被 打 断 。是 一 个 门 的 输 入 到 输 出 之 间 的 延 时 。 是 时序 分 析 路 径 上 一 个 元 件 的 输 出 到 下 一 个 元 件 输 入 之 间 的 路 径 延时 （ 寄 生 电 容 ， 线 电 阻 ， 驱 动 强 度 等 都 会 引 起 延 时 ） 。goon from here 06.11.22 Page 55 4.4.2 静 态 时 序 分 析 中 的 基 本 概 念 1. 扇 入 和 扇 出 一 个 逻 辑 门 的 是 指 连 接 到 该 门 输 入 的 数 目 ， 一 个 逻辑 门 的 是 指 连 接 到 该 门 输 出 的 负 载 门 的 数 目 ， 扇 出 越多 ， 延 时 越 大 。 . N .M Page 56 4.4.2 静 态 时 序 分 析 中 的 基 本 概 念2. 压 摆 率 (slew rate) 压 摆 率 (slew rate): 电 压 变 化 的 速 度 。 )( %80)( fr OLOH TTVVdtdV Page 57 4.4.2 静 态 时 序 分 析 中 的 基 本 概 念3. 时 钟 歪 斜 (clock skew) 时 钟 在 经 过 时 钟 路 径 后 ， 到 达 存 储 元 件 的 时 间 存 在 差 别 ，称 为 。 时 序 上 相 邻 的 寄 存 器 如 果 时 钟 歪 斜 较 大 ，可 能 在 同 一 时 钟 沿 上 造 成 时 间 违 规 或 不 能 正 确 锁 定 数 据 的现 象 。 Page 58 4.4.2 静 态 时 序 分 析 中 的 基 本 概 念4. 寄 存 器 的 建 立 (ts)和 保 持 时 间 (th)寄 存 器 的 建 立 和 保 持 时 间 的 验 证 是 静 态 时 序 分 析 最 重 要的 参 数 。 所 谓 的 是 指 一 个 数 据 信 号 在 有 效 的 时 钟沿 到 达 前 必 须 稳 定 的 最 小 时 间 ； 是 指 一 个 数 据 信号 在 有 效 时 钟 沿 结 束 后 必 须 稳 定 的 最 短 时 间 。 Page 59 4.4.2 静 态 时 序 分 析 中 的 基 本 概 念5. 时 钟 到 输 出 的 延 时 （ tco）时 钟 到 输 出 的 延 时 是 指 信 号 通 过 寄 存 器 传 播 到 输 出 管 脚后 ， 在 输 出 管 脚 上 获 得 稳 定 有 效 的 数 据 所 要 求 的 最 大 时 间 。6. 时 钟 脉 冲 宽 度 时 钟 脉 冲 宽 度 定 义 为 一 个 时 钟 周 期 的 高 /低 电 平 的 最 小 宽度 。 如 果 脉 冲 宽 度 过 小 ， 那 么 存 储 器 就 不 能 正 确 锁 存 数 据 。 脉 冲 宽 度 Page 60 4.4.2 静 态 时 序 分 析 中 的 基 本 概 念7.恢 复 (Recovery)数 据 /撤 销 (Removal)数 据 时 间 时 钟 有 效 沿 前 ， 异 步 控 制 输 入 信 号 （ 如 reset, clear） 必须 稳 定 的 最 小 时 间 称 为 恢 复 时 间 。 时 钟 有 效 沿 后 ， 异 步 控 制输 入 信 号 （ 如 reset, clear） 必 须 稳 定 的 最 小 时 间 称 为 撤 销 时间 。 如 果 时 钟 有 效 沿 和 异 步 复 位 信 号 的 结 束 之 间 的 时 间 太 短 ，寄 存 器 无 法 判 断 是 继 续 保 持 复 位 值 ， 还 是 该 由 时 钟 沿 打 入 新的 数 据 ， 从 而 导 致 寄 存 器 的 内 容 不 确 定 。 RESETCLK Removel RESETCLK Recovery恢 复 时 间撤 销 时 间 Page 61 4.4.2 静 态 时 序 分 析 中 的 基 本 概 念8. 裕 度 (slack) 裕 度 是 时 序 要 求 与 实 际 时 序 之 间 的 差 值 ， 它 反 映 了 时 序是 否 满 足 要 求 。 （ 的 裕 度 表 示 设 计 满 足 时 序 要 求 ， 而 的裕 度 表 示 设 计 不 满 足 时 序 要 求 。 ） 裕 度 = 要 求 的 时 间 实 际 的 时 间 9. 最 大 时 钟 频 率 最 大 时 钟 频 率 是 指 在 不 违 背 要 求 的 建 立 和 保 持 时 间 前 提下 ， 电 路 工 作 的 最 快 速 度 。 频 率 1/最 大 的 时 钟 周 期 Page 62 4.4.3 假 路 径 和 多 周 期 路 径 n 假 路 径 静 态 时 序 分 析 工 具 对 于 假 路 径 不 能 正 确 分 析 。 逻 辑 门 的 控 制 值 和 非 控 制 值 如 果 一 个 逻 辑 门 的 输 出 值 只 取 决 于 一 个 输 入值 ， 这 个 输 入 值 就 是 该 逻 辑 门 的 控 制 值 ， 而 其它 值 则 为 非 控 制 值 。 例 如 ， “ 与 ” 门 的 控 制 就是 0， 非 控 制 值 是 1， 而 “ 或 ” 门 的 控 制 值 是 1，0为 非 控 制 值 。 Page 63 4.4.3 假 路 径 和 多 周 期 路 径 路 径 敏 化 （ 静 态 可 敏 化 /动 态 可 敏 化 ） ： 对 于 一 条 路 径 ， 如 果 存 在 一 组 输 入 向 量 使 得该 路 径 上 逻 辑 门 的 其 他 输 入 都 被 设 置 成 非 控 制 值 ， 则 这 条路 径 称 为 是 可 敏 化 路 径 。 y b ea c d zb=0、 1都 是 控 制 值 ， acdz不 可 敏 化 （ 也 就 是 说 从 输 入 a到 z不能 传 递 任 何 信 号 的 跳 变 ） ， 如 果 一 条 路 径 是 静 态 不 可 敏 化 ，那 么 这 条 路 径 对 于 延 时 分 析 是 没 有 贡 献 的 ， 把 这 种 路 径 称 为是 假 路 径 。 Page 64 ： 如 果 在 一 条 路 径 上 ， 在 不 同 的 时 间 可 以 找 到 一组 输 入 ， 使 得 这 条 路 径 可 以 传 输 信 号 的 跳 变 ， 这 种 敏化 方 式 称 为 动 态 可 敏 化 。 4.4.3 假 路 径 和 多 周 期 路 径 n 多 周 期 路 径 Page 65 4.4.3 假 路 径 和 多 周 期 路 径 n 静 态 时 序 分 析 由 FPGA开 发 系 统 中 的 静 态 时 序分 析 工 具 自 动 完 成 ， 用 户 根 据 电 路 的 特 点 ， 向静 态 时 序 分 析 工 具 提 交 时 序 约 束 文 件 ， 静 态 时序 分 析 工 具 计 算 所 有 的 可 能 的 路 径 ， 检 查 电 路设 计 是 否 满 足 时 序 要 求 ， 并 给 出 详 细 的 分 析 报告 。 用 户 根 据 此 报 告 ， 对 电 路 进 行 判 定 或 修 改 。n 用 户 通 过 约 束 文 件 可 以 对 设 计 的 多 周 期 路 径 或者 假 路 径 进 行 指 定 方 式 的 控 制 或 不 进 行 控 制 。