极客工场

Appearance

共 4,262 字预计阅读约 14 分钟

SVA 检查 AXI 握手：两条关键断言实跑，抓出从机 RTL 的真 bug ​

更新时间：2026-10-28。本文是「集成电路大类 · 芯片设计」中间层（intermediate）的一篇实验文。AXI 的 valid/ready 握手规则在 valid/ready 握手：反压、气泡、Skid Buffer 与 AXI-Stream 基础 里已经讲过语义，AXI4-Lite 从机设计：寄存器读写、五通道握手与地址解码 给了一个能跑仿真的从机实现，AXI-Lite 从机回归实测 用 cocotb 做过随机回归。但仿真回归只覆盖你打过的激励——协议规则本身对不对，应该交给断言去盯。本篇把两条最关键的规则写成 SVA：valid 一旦举起、握手完成前不许撤；通道被 stall 期间、数据不许变。然后不用仿真器，用形式验证（yosys-smtbmc + z3）穷举所有输入序列去证它们。结果是：手里这份在仿真回归里一直全绿的从机 RTL，被断言当场抓出一个真 bug。

本文要回答的问题 ​

  • AXI 握手那么多条规则，最值得写成断言的是哪两条？对应的 SVA 长什么样？
  • 断言挂在被测模块的什么位置，形式工具才看得见？
  • 一个「仿真全绿」的从机，为什么会在形式验证里翻车？翻在哪一拍？
  • BMC（有界模型检查）报 FAILED 之后，怎么从反例波形读出根因并修复？

先把这次实验的结局摆出来，左右两栏的每一条都能在正文日志里找到出处：

同一份从机 RTL：修复前被断言抓挂，修复后 20 步归纳通过

这张卡要读的重点不是「挂了又好了」这个结果，而是改动的粒度：左边那列的所有症状——二次接收 AR、rdata 被覆盖、断言报挂——收敛到右边一个条件项 && !arready。协议 bug 的可怕之处就在于它藏在一个看起来人畜无害的握手表达式里，仿真激励不凑巧打不中那个窗口，而断言把它钉死在数学上。

一、被测对象与两条关键断言 ​

被测对象是一个教学级 AXI4-Lite 从机 axi_lite_regs：四个 32 位寄存器，五通道齐备（AW/W/B 写、AR/R 读），读通道的核心逻辑就两行——arready 在「有地址请求且当前没有读数据挂着」时举起，rd_fire（arvalid 与 arready 同拍为高）时把寄存器值装进 rdata 并举起 rvalid。这类代码在任何 AXI-Lite 教程里都能见到，长相极其标准。

AXI 协议对 valid/ready 的约束很多，但对从机最要命的是这两条：

  1. valid 举起后不许撤：rvalid 一旦拉高，在 rready 拉高完成握手之前必须保持为高。撤回了，主机就永远丢了这笔数据——它可能正等着 rvalid 再举一次。
  2. stall 期间数据不许变：rvalid && !rready 的每一拍，rdata 必须 bit 级保持稳定。主机在 stall 期间可能已经在多拍里对 rdata 采样做跨域同步或总线桥转，数据中途变脸等于发了一笔坏数据。

这两条写成 checker 模块如下（B 通道的 bvalid 同理，一并挂上凑成三条）：

systemverilog
// axi_lite_checker.sv — 挂在从机信号上的三条协议断言
module axi_lite_checker (
    input  wire        aclk,
    input  wire        aresetn,
    input  wire        rvalid,
    input  wire        rready,
    input  wire [31:0] rdata,
    input  wire        bvalid,
    input  wire        bready
);
    // A1: rvalid 举起后，握手完成前不许撤
    always @(posedge aclk)
        if (aresetn && $past(aresetn))
            assert (!($past(rvalid) && !$past(rready)) || rvalid);
    // A2: stall 期间 rdata 必须保持稳定
    always @(posedge aclk)
        if (aresetn && $past(aresetn))
            assert (!($past(rvalid) && !$past(rready)) || $stable(rdata));
    // A3: bvalid 同样不许在 bready 之前撤回
    always @(posedge aclk)
        if (aresetn && $past(aresetn))
            assert (!($past(bvalid) && !$past(bready)) || bvalid);
endmodule

三段断言的结构一模一样：守卫条件 $past(rvalid) && !$past(rready) 表示「上一拍 valid 举着但没被接收」，此刻就进入了协议的锁定期；A1 要求当前拍 rvalid 仍为高，A2 要求 rdata 与上一拍逐位相等。$past 是取上一拍采样值的系统函数，它的语义细节与坑在 SVA $past 函数：采样历史值写断言的语义、门控时钟参数与四个常见坑 里专门讲过，本篇后面会亲眼撞上其中一个。

checker 写好了，挂在哪、用什么工具证，一张图说清整条链路：

d2
direction: right
top: "formal_top 验证外壳" {
  dut: "axi_lite_regs 从机\nAW/W/B/AR/R 五通道\n4 × 32 位寄存器组"
  chk: "axi_lite_checker\nA1 rvalid 不许撤\nA2 stall 期间 rdata 稳定\nA3 bvalid 不许撤"
  dut -> chk: "rvalid/rready/rdata\nbvalid/bready 抽头"
}
syn: "yosys 0.30\nprep -top formal_top\nwrite_smt2 位级展开"
smt: "yosys-smtbmc + z3\nBMC 20 步\n时序归纳"
top -> syn: "读入 DUT 与 checker"
syn -> smt: design.smt2
dut.style: { fill: "#FEF3E2"; stroke: "#E08A1E" }
chk.style: { fill: "#FDECEC"; stroke: "#D9534F" }
syn.style: { fill: "#EAF2FE"; stroke: "#3B6FD4" }
smt.style: { fill: "#E9F8F0"; stroke: "#2E9E6B" }

读这张图抓住三个角色：橙色是设计与断言的挂载关系——checker 不改 DUT 一行业务代码，只从五个信号上抽头旁观；蓝色是前端编译，yosys 把整个外壳位级展开成 SMT-LIBv2 公式；绿色是证明后端，z3 求解器回答「存不存在一段输入序列让某条断言为假」。这里有一个对结果影响巨大的工程细节：checker 必须用 wrapper 模块直接例化，不能用 SystemVerilog 的 bind——实测里 bind 挂上去的断言在 yosys 0.30 的 write_smt2 阶段根本不会进 SMT 公式，等于证了个空设计。所以 formal_top 把 DUT 与 checker 并排例化、同名信号直连，保证三条断言出现在最终的公式里。

二、为什么是形式验证而不是再多打点仿真激励 ​

这个问题值得正面回答，因为它决定了本篇的方法论选择。仿真（包括 AXI-Lite 从机回归实测 那样的 cocotb 随机回归）的覆盖逻辑是「我打了什么激励，就检查什么行为」——定向激励测设计者的想象，随机激励测伪随机数发生器的运气。rdata 被覆盖这种 bug 需要一个非常具体的窗口：前一笔读数据举着、主机恰好不接收、同时主机把下一笔 AR 已经顶到门口，三个条件同拍成立。随机回归里这三个事件各自都常见，但同拍对齐的概率极低，跑几百笔可能一次都撞不上。

形式验证把问题反过来问：求解器自由选取每一拍的全部输入组合（arvalid、araddr、rready 都是自由变量），只要存在任何一段合法序列让断言为假，就返回这段序列作为反例。覆盖不再是概率问题，而是数学问题。代价是状态空间爆炸——好在 AXI4-Lite 从机这种几十个触发器的小模块，对现代 SMT 求解器是甜点区。想系统入门 assert/assume/cover 与有界证明的分工，可以看 形式验证入门：assert/assume/cover、bounded proof 与 FIFO/仲裁器验证。

三、第一次实跑：断言在第 1 步就把原始 RTL 抓挂 ​

对原始 RTL（不加任何修改）跑 BMC，深度 20 步。结果出乎意料地快：

原始 RTL 实跑：BMC 第 1 步断言 FAILED

这份实录按行读：求解器 z3 上场后，第 0 步、第 1 步逐拍检查断言，第 1 步还没查完就报 BMC failed!——栽在 axi_lite_checker.sv 第 13 行，正是 A1「rvalid 不许撤」那条。工具把反例波形写成 VCD，最后状态行 Status: FAILED (!) 盖棺。深度 20 的 BMC 在第 1 步就翻车，说明违例序列短得可怜。

把反例 VCD 译成拍点表（信号取 DUT 与 checker 两侧同名的读通道与复位信号）：

拍aresetnarvalidarreadyrvalidrready说明
010100复位已释放，arready 悬空为高，rvalid 为低
100000复位重新拉起，全通道清空

这个反例的第一层信息是个经典现象：BMC 从任意状态起跑，这份反例里设计从头到尾没经历过一次完整的复位序列，第 0 拍复位就已经释放了。A1 在第 0 拍回看 $past(rvalid) 时，取到的是求解器自由编造的历史——「上一拍 rvalid 举着且没人接收」，而当前拍 rvalid 为低，断言立刻报挂。这正是 $past 与「无复位起跑」组合出的典型假反例，SVA $past 函数 里把它列为头号坑。正经做法是让复位先拉低若干拍再释放，或用 assume 约束起跑状态。

但这次不能到此为止——顺着 FAIL 回头逐行复审 RTL，一个与假反例无关的真 bug 浮出水面。看原始代码的 arready 生成逻辑：

systemverilog
// 原始 axi_lite_regs.v 的读地址通道
arready <= arvalid && !rvalid;

arready 是打了一拍的寄存器输出：本拍看到 arvalid && !rvalid，下一拍举起 arready。问题出在 !rvalid 用的是本拍的 rvalid。设想主机背靠背发读、且第一笔数据它暂不接收：

  • 第 1 拍：arvalid=1、rvalid=0 → arready 将在第 2 拍举起；
  • 第 2 拍：arready=1，arvalid 仍举着（主机在等握手），rd_fire 成立，rdata 装入 D1，rvalid 将在第 3 拍举起。同一拍，arready <= arvalid && !rvalid 里的 rvalid 还是 0（rvalid 第 3 拍才变 1），于是 arready 第 3 拍继续为高；
  • 第 3 拍：rvalid=1、rready=0（stall 开始），但 arready=1 且主机下一笔 arvalid 已在门口——第二笔 AR 被接收，rd_fire 再次成立，rdata 将在第 4 拍被 D2 覆盖；
  • 第 4 拍：rvalid 仍举着、rready 仍低，rdata 却已经从 D1 变成了 D2。主机最终读到的是第二笔的地址译码结果，第一笔数据被无声吞掉。

这正是 A2 要盯的违例：stall 期间 rdata 变了。把这个窗口画成波形，比文字更直观：

chip-design/verification/sva-check-axi-lite-sby.md 波形时序图

读这张波形抓住违例窗口：第 2、3 拍 arready 连续两拍为高（这就是 !rvalid 看旧值漏出的窗口），第二笔 AR 在第 3 拍被收走；第 3 拍起 rvalid=1 && rready=0 进入 stall，而 rdata 在第 4 拍从 D1 跳到 D2——stall 期间数据不许变这条铁律被踩破。从第 4 拍往后，无论主机哪一拍拉起 rready，读走的都是被污染的 D2。

为什么仿真回归一直没抓到它？因为条件太苛刻：主机要背靠背发两笔读、第二笔地址必须恰好顶在前一笔 rvalid 举起的同一拍、且主机此刻恰好不拉 rready。cocotb 回归里主模型（bus driver）通常拿到数据立刻 rready，stall 本就稀少，更别说与背靠背 AR 对齐。断言不看概率，所以这个窗口被一击命中。

四、修复：一个条件项封死双收窗口 ​

根因清楚了，修法就顺理成章：arready 不该「看 rvalid 的旧值决定下一拍举不举」，而应该只举一拍——举过就歇，等 rd_fire 把读数据真正挂起之后再议。在条件里追加 && !arready：

systemverilog
// 修复版 axi_lite_regs_fixed.v —— arready 单拍化
arready <= arvalid && !rvalid && !arready;

逐拍推演修复效果：第 2 拍 arready=1 完成第一笔 AR 接收后，由于 !arready 为假，第 3 拍 arready 必定回落为 0；第 3 拍起 rvalid=1 又把条件里的 !rvalid 堵死，arready 在整个读数据挂着期间都不可能再举。同一时刻至多一笔读事务在飞，rdata 在 stall 期间物理上失去了被改写的路径。

重新走一遍完整流程，这次换成修复版 RTL：

修复版实跑：20 步 BMC 加时序归纳 PASSED

这次的日志形态与上次完全不同：没有逐拍 Checking assertions 的爆裂声，而是从 20 步倒着往 17 步做时序归纳（temporal induction），归纳在有限深度内闭合，Temporal induction successful 加上 Status: PASSED。时序归纳的含义是：不仅前 20 拍内不存在违例，而且「任意满足断言的 k 拍历史之后，第 k+1 拍仍满足」也被证明——这把结论从「有界安全」升级成「任意深度安全」，比单纯 BMC 的 PASSED 硬得多。归纳深度怎么选、证不动时怎么加不变量，k 归纳证明：归纳深度选择、不变量加强技巧与 BMC 组合的实战方法论 有完整讨论。

前后两份日志并排看，有个细节值得玩味：抓挂原始 RTL 只用了两步 BMC，证明修复版安全却动用了 20 步归纳。找 bug 便宜、证无 bug 贵，这是形式验证的成本结构，也是它和仿真互补而不是互替的原因——断言负责穷举，仿真负责覆盖工具链够不着的大状态空间。

五、两个工具链坑：sby 版本错配与 bind 的静默失效 ​

流程层面这次踩了两个坑，都比 bug 本身更容易浪费后来者的时间，如实记录。

坑一：sby 与 yosys 0.9 不兼容。 SymbiYosys（sby）本是这套流程的标准前端——一个 .sby 文件声明文件列表、深度、引擎，sby -f pass.sby 一键跑完。但实验镜像里的 sby 与宿主 yosys 0.9 在脚本生成上互不兼容，跑不起来。替代方案是把 sby 内部干的事手工拆成两段：先在容器里用 yosys 0.30 做前端编译（read -formal 读入、prep 展平、write_smt2 导出位级公式），再在宿主用 yosys-smtbmc 0.9 加 z3 4.8.12 做求解。sby 的本质就是这两段的编排器，手工拆开后语义完全等价，只是没了自动化的壳。

坑二：bind 挂 checker，断言不进 SMT 公式。 一开始按教科书姿势写 bind axi_lite_regs axi_lite_checker chk (...)，形式验证秒过——快得可疑。插了一根金丝雀探针（一条 assert(1'b0)，永假断言）验证流程有效性：连永假断言都 PASS，说明断言根本不在被证明的公式里。yosys 0.30 的 write_smt2 不展开 bind 进去的模块实例。改成 wrapper 模块 formal_top 并排例化 DUT 与 checker 后，金丝雀立刻 FAILED（证明公式里真有断言），撤掉金丝雀后才是有效的 PASSED。形式验证跑 PASS 的第一反应应该是怀疑它什么都没证——用永假断言做空转检查，是每次搭流程都必须做的一次自检。这类「PASS 但什么都没测到」的空真问题，SVA 断言实战：sequence/property、握手协议检查与空真断言陷阱 从仿真侧也讲过一遍。

环节正确姿势本次踩坑
流程编排sby 一键，或手工 yosys + smtbmc 两段镜像内 sby 与 yosys 0.9 不兼容，改两段式
checker 挂载wrapper 模块直接例化bind 不进 write_smt2，断言静默缺席
PASS 自检先插 assert(1'b0) 金丝雀应 FAIL金丝雀 PASS 暴露 bind 失效
起跑状态复位先拉低若干拍，或 assume 约束无复位起跑，$past 窗口给出假反例

这一篇在知识体系里的位置 ​

一句话总结 ​

SVA 检查 AXI 握手，最值得写死的是两条：valid 举起后握手完成前不许撤、stall 期间数据不许变。本篇把这两条（外加 bvalid 一条）挂在 axi_lite_regs 从机上，用 yosys-smtbmc 加 z3 实跑：原始 RTL 的 arready <= arvalid && !rvalid 因看旧值漏出双收窗口，背靠背 AR 加 stall 同拍对齐时 rdata 被覆盖，断言 FAIL；修复版追加 && !arready 让 arready 单拍化，20 步 BMC 加时序归纳 PASSED。方法论上记住三件事：checker 用 wrapper 例化别用 bind、PASS 先过 assert(1'b0) 金丝雀自检、$past 断言要配复位序列否则 BMC 起跑就出假反例。

实验环境 ​

  • 机器/系统：eda-golden-v1 镜像 / Ubuntu 22.04（yosys 0.30 在 OpenLane 容器内运行，yosys-smtbmc 与 z3 在宿主）
  • 工具版本：Yosys 0.30+48（git sha1 14d50a176d5，版本行照抄日志）、yosys-smtbmc 0.9、z3 4.8.12
  • 日期：2026-10-28
  • 完整命令序列：
bash
# 第一段：容器内 yosys 0.30 前端编译，导出 SMT-LIBv2（原始 RTL）
yosys -p "read -formal -sv axi_lite_regs.v axi_lite_checker.sv formal_top_orig.sv; prep -top formal_top_orig; write_smt2 -wires design.smt2"
# 第二段：宿主 yosys-smtbmc + z3 做 20 步 BMC —— FAILED（原始 RTL）
yosys-smtbmc -s z3 -t 20 -m formal_top_orig design.smt2
# 修复版：同法编译 formal_top.sv（DUT 换 axi_lite_regs_fixed）
yosys -p "read -formal -sv axi_lite_regs_fixed.v axi_lite_checker.sv formal_top.sv; prep -top formal_top; write_smt2 -wires design.smt2"
# 修复版：20 步 BMC + 时序归纳 —— PASSED
yosys-smtbmc -s z3 -t 20 -i -m formal_top design.smt2

代码获取 ​

完整 RTL（原始版、修复版、故意坏版）、checker、wrapper 与流程脚本已同步到公开仓库：geek-doc.cn/experiments/sva-check-axi-lite-sby，克隆后进入该目录按 README 执行两段式命令（需 yosys 与 yosys-smtbmc、z3）即可复现本文 FAILED 与 PASSED 两份结果。