极客工场

Appearance

共 1,070 字预计阅读约 4 分钟

SVA 断言基础：即时断言与并发断言的分工，以及一条并发断言的 FAIL/PASS 形式化实证 ​

更新时间：2026-10-28。本文是「集成电路大类 · 芯片设计」中间层（intermediate）的一篇实验文。SVA 断言基础这个主题，概念侧本站在 SVA 断言实战 与 形式化验证基础 里已经铺过语法与方法论；本篇不重复语法手册，而是抓住新手最容易栽的一个分界问题——即时断言（immediate assertion）和并发断言（concurrent assertion）到底各管什么——然后用一个 30 行的 req/ack 握手设计，在开源形式化工具链上把同一条并发断言分别跑出 FAILED 与 PASSED 两份真实记录。断言不是写出来就算数的，能被工具证伪、也能被工具证真，才算真正理解它。

本文要回答的问题 ​

  • 即时断言和并发断言在「什么时候求值、能表达什么」上的本质差别是什么？
  • 一条「请求之后一拍必须给应答脉冲」的规格，为什么只有并发断言（或等价的带 $past 的时序检查）才写得出来？
  • 形式化工具跑一条并发断言，FAILED 时给的反例长什么样、怎么读？
  • assert 和 assume 的角色为什么不能写反？

先把本篇两类断言的分工摆在一起对比，这是全篇的概念骨架：

SVA 断言基础第一课：即时断言管当下，并发断言管跨拍

读这张卡抓住右边一栏的最后一行：并发断言与即时断言最实用的差别不在语法，而在谁能进形式化工具。即时断言的执行依赖仿真激励走到那一行，形式化工具穷举状态空间时不会替你「执行」过程块里的 printf 式检查；而并发断言（以及本文实验里用的带 $past 的 always 断言）会被综合成形式化模型里的 $assert 单元，参与有界模型检验（BMC）与归纳证明。换句话说：想被工具「证明」，就得写成工具认账的形式。

一、被测规格：一句话的 req/ack 握手契约 ​

实验设计刻意做到最小，让 FAIL 与 PASS 的差别一目了然。规格只有两句话：请求方把 req 拉高并保持到收到 ack；被测方收到请求后，恰好在下一拍给一个单拍的 ack 脉冲——不能早、不能晚、不能多拍。

好设计与坏设计的 RTL 只差半行：

systemverilog
// req_ack_good.v：ack 恰为单拍脉冲
always @(posedge clk) begin
    if (!rst_n) ack <= 1'b0;
    else        ack <= req && !ack;   // 上一拍 ack 高过就撤回
end

// req_ack_bad.v：BUG —— ack 跟随 req，req 保持几拍 ack 就高几拍
always @(posedge clk) begin
    if (!rst_n) ack <= 1'b0;
    else        ack <= req;
end

这个 bug 在现实中非常典型：握手逻辑里忘了「脉冲化」，应答信号变成电平跟随。功能仿真里如果 testbench 对 ack 只做「等到高电平就继续」的检查，这个 bug 完全测不出来——多打的拍被容忍掉了。它属于规格级错误而非功能级错误，恰好是断言的主场。

两条检查写成并发风格的断言（`ifdef FORMAL 包裹，只在形式化模式下生效）：

systemverilog
// A1：ack 当且仅当「上一拍有未应答的请求」时为高——不多不少
always @(posedge clk)
    if (rst_n && $past(rst_n))
        assert (ack == ($past(req) && !$past(ack)));
// A2：req 为低时不许凭空冒 ack
always @(posedge clk)
    if (rst_n)
        assert (!ack || req);

注意 A1 里 $past 的用法：它把「上一拍」这个跨拍概念显式拉进表达式，这正是并发断言相对即时断言的核心能力。即时断言只能写 assert (ack == req) 这种同拍判断，表达不了「上一拍请求、这一拍才应答」的时序契约。对输入侧 req 的约束则写成 assume：请求方保持 req 直到收到 ack、收到后立即撤销——对输入写 assume、对输出写 assert，这个分工写反了工具就会把「环境不给 req」也当成设计的错。

assume 还有一个方向的坑：写少了，求解器会构造出「诡异但合法」的激励把断言打爆，比如 req 永远不来、ack 无从谈起；写多了（过约束），把本该覆盖的输入序列也禁掉，PASSED 就变得没有意义。经验法则是 assume 只描述接口协议允许的行为，一条都别多。本实验的两条 assume 恰好是协议的另一半——「保持到应答」加「应答后撤销」，少一条，坏设计的反例会更花哨，好设计的归纳也未必能闭合。

二、坏设计被抓包：反例时序逐拍读 ​

先跑坏设计。工具链分两阶段（原因见后文「工具链的坑」）：先用 yosys 把 RTL 与断言一起转成 SMT-LIBv2 模型，再交给 SMT 求解器做有界模型检验。结果一句话：BMC 在第 1 步就把两条断言全部打爆。

反例的时序关系画成波形最直观：

chip-design/verification/sva-assertion-basics-sby.md 波形时序图

读这张图抓住 ack 两行的高电平宽度：好设计的 ack 只在请求后的那一拍出现一次（一个周期宽），坏设计的 ack 从请求到达后一直跟随 req，req 保持 4 拍它就高 4 拍。最下面一行是断言 A1 的逐拍判定：ack == ($past(req) && !$past(ack)) 这个等式在 req 保持的第二拍及以后全部不成立——左边 ack 仍是 1，右边因为 $past(ack) 已经是 1 而变成 0，等式断裂，断言失败。求解器给出的正是这样一条「req 持续多拍」的反例轨迹。

实际日志原文摘录如下，注意两个 $assert 单元在第 1 步就双双触发：

exp-log
##   0:00:00  Solver: z3
##   0:00:00  Checking assertions in step 0..
##   0:00:00  Checking assertions in step 1..
##   0:00:00  BMC failed!
##   0:00:00  Assert failed in req_ack_bad: $assert$req_ack_bad.v:23$44
##   0:00:00  Assert failed in req_ack_bad: $assert$req_ack_bad.v:27$45
##   0:00:00  Writing trace to VCD file: trace.vcd
##   0:00:00  Status: FAILED (!)

这段输出值得记住两个细节。其一，Assert failed in req_ack_bad: $assert$req_ack_bad.v:23$44 里的 :23 就是源文件行号——A1 写在第 23 行、A2 在第 27 行，工具把内部生成的 $assert 单元名与源码位置对应起来，定位不需要猜。其二，失败发生在 step 1 而不是 step 19：这说明 bug 很「浅」，从复位释放后一拍就能构造出反例，BMC 深度 20 绰绰有余。顺带一提，前半段 yosys 的统计也透露了形式化模型的规模：整个设计综合后只有 16 个触发器、2 个 $assert、2 个 $assume——这种小设计求解器秒出结果，是学习形式化的理想起步规模。

反例落盘的 VCD 里只有四个信号：clk、rst_n、req、ack，外加一个求解器内部的步数标记。这正是形式化反例与仿真波形的观感差别——没有 testbench 打出的横幅、没有无关内部信号，就是一条最短的「罪证轨迹」：从复位释放到断言断裂的每一拍输入取值。拿到 FAILED 后第一件事就是打开这条轨迹，对照断言表达式逐拍代入验算；如果代入后等式其实成立，那多半是 assume 写少了、轨迹里有协议不允许的激励，回头补环境约束，而不是急着改 RTL。

三、修好之后：从 FAILED 到归纳证明 PASSED ​

把 ack <= req 改成 ack <= req && !ack，同样的命令再跑一遍。这次 BMC 20 步走完没找到任何反例，工具接着做时序归纳（temporal induction）——证明「如果任意时刻前若干拍断言成立，则下一拍也成立」，一旦归纳步闭合，断言就不只是「前 20 拍没被打爆」，而是对所有可能的输入序列、任意长的运行都成立：

好设计：BMC 20 步无反例，时序归纳成功

Temporal induction successful. Status: PASSED 这两行是形式化验证里最有分量的结论：仿真一万次 PASS 只能说明「这一万种激励没踩中雷」，归纳 PASSED 则是数学意义上的「不存在踩雷的激励」。值得把 BMC 与归纳的差别说透，因为命令行上只差一个 -i 开关：BMC（有界模型检验）回答的是「在前 N 步之内有没有反例」，它是证伪工具，找不到反例不代表没有，只代表雷埋得比 N 深；归纳回答的是「对任意深度都没有反例」，它是证真工具，前提是归纳步能闭合——也就是从「断言在任意连续 k 拍成立」能推出「第 k+1 拍也成立」。本设计状态只有 16 个触发器、逻辑深度很浅，归纳在 20 步深度上一次闭合；换成深流水线的设计，归纳可能闭不上，那时结论会停在「BMC 20 步无反例」，强度弱一档，报告时务必分清自己拿到的是哪一种。

对照同一条命令在坏设计上的输出：

坏设计：BMC 第 1 步双断言触发，落盘反例 VCD

两份记录并排放，断言工程的完整闭环就齐了：写断言 → 故意留 bug 验证断言能抓（FAILED 带反例）→ 修 bug → 证明断言通过（PASSED）。跳过第一步直接看 PASSED 是新手最常见的自我欺骗——一条永远打不中的断言，可能只是写错了永远求值为真。先证伪、再证真，断言才算真正「上岗」。

四、工具链的两个真实坑 ​

实验过程里踩到两个坑，比正文结论更值得带走。

第一个坑在版本兼容。本打算用 SymbiYosys（sby）一键跑，但环境里的 sby（git HEAD）生成的脚本含有 hierarchy -smtcheck、write_jny 等新命令，配套的 yosys 0.9 一概不认识，第一轮直接以返回码 16 收场。解决办法是把 sby 的 smtbmc 引擎手工拆成两段：用较新的 yosys 0.30 做 read -formal -sv + prep -top + write_smt2 -wires 生成模型文件，再交给宿主的 yosys-smtbmc + z3 求解。形式化流程本质是「前端翻译 + 后端求解」两段式，卡住时拆开手工走一遍，往往比折腾版本对齐更快。

第二个坑更隐蔽：checker 挂接方式决定断言会不会进模型。早期尝试用 bind 把断言模块挂到被测设计上，结果模型里根本没有 $assert 单元——连埋进去的金丝雀断言 assert(1'b0)（一条必炸的探针）都显示 PASSED，这才暴露断言压根没进 SMT2 文件。改成 wrapper 直接例化后断言才被翻译进去。教训可以推广成一条纪律：任何形式化跑出的 PASS，先用一条必失败的探针断言确认检查链路是通的，否则你可能只是在为一台没插电的机器欢呼。

症状真实根因对策
sby 第一轮 rc=16sby git HEAD 与 yosys 0.9 命令集不兼容拆成 yosys 0.30 前端 + smtbmc 后端手工两段流
金丝雀 assert(1'b0) 也 PASSbind 挂接的 checker 未翻译进 smt2改 wrapper 例化；PASS 必先探针验证
断言写法 |=> 不支持该链路只认 immediate + $past 形式序列改写为带 $past 的布尔等式

五、即时断言与并发断言怎么选 ​

回到开头的问题，给一条可执行的判据：这个检查涉及「拍」这个概念吗？

  • 不涉及——只是「这个指针不该为空」「这个除数不能是零」「当前状态机不该在这个状态」这类同一时刻的布尔判断，写即时断言，放在过程块里，仿真期立即报错，成本最低。
  • 涉及——「请求后 N 拍内必须应答」「grant 拉起期间 req 不许撤」「写使能与片选必须同拍」这类跨拍契约，写并发断言；它不仅能在仿真里每拍自动求值，还能原样进形式化工具被穷举证明。

工程上还有一个常被忽视的收益：并发断言是可执行的规格文档。req/ack 这个例子里，A1 那一行等式比任何注释都精确地定义了「单拍脉冲应答」的含义——注释会腐烂，断言每次回归都被重新验证。这也是 基于断言的验证方法论 一直强调的：断言密度本身就是一种验证资产。更深一层的 assume/assert/cover 三角关系，可以接着读 assert、assume 与 cover 在形式化中的分工；本篇的 assume 写法正是那篇讲的「环境建模」最小实例。

给准备动手的读者一份最小起步清单，按顺序勾完就算入门：第一，挑一个 20 行以内、带握手的小模块（req/ack、valid/ready 均可），别一上来就对着真实 IP 核写断言；第二，把规格里每一句「必须」「不许」各翻成一条断言，本篇的 A1、A2 就是「恰好一拍脉冲」与「不许无中生有」两句话的直译；第三，先故意留一个 bug 跑出 FAILED，确认断言能咬人，再修掉看 PASSED；第四，每次拿到 PASS 都问一句「检查链路通不通」——金丝雀断言探活应成为肌肉记忆。这四步全走完，你对断言的理解就超过了只背语法的多数人。

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

一句话总结 ​

SVA 断言基础的分水岭在「是否跨拍」：同拍判断用即时断言、时序契约用并发断言，而后者才能进形式化工具被穷举证明。本篇在一个 16 触发器的 req/ack 设计上实测完整闭环：坏设计 ack <= req 被 BMC 第 1 步双断言打爆（FAILED + 反例 VCD），修成 ack <= req && !ack 后时序归纳 PASSED；并实录了两个真坑——sby 与 yosys 版本不兼容需拆两段流、bind 挂接的断言不进模型须以金丝雀断言探活。任何 PASS，先确认它有能力 FAIL。

实验环境 ​

  • 机器/系统：云主机 16C32G / Ubuntu 22.04（eda-golden-v1 镜像）
  • 工具版本：Yosys 0.30+48（git sha1 14d50a176d5，OpenLane docker 镜像内，负责 prep/write_smt2）；yosys-smtbmc 0.9（宿主）；z3 4.8.12（求解器）
  • 日期：2026-10-28
  • 完整命令序列：
bash
# 前端：RTL + 断言 → SMT-LIBv2 模型（OpenLane docker 内 yosys 0.30）
sudo docker run --rm -v /tmp:/tmp -w $PWD efabless/openlane:<sha>-amd64 \
  yosys -p "read -formal -sv req_ack_bad.v; prep -top req_ack_bad; write_smt2 -wires design.smt2"
# 后端：BMC 20 步，带反例 VCD 落盘（坏设计，FAILED）
yosys-smtbmc -s z3 -t 20 --dump-vcd trace.vcd -m req_ack_bad design.smt2
# 后端：prove 模式 = BMC + 时序归纳（好设计，PASSED）
yosys-smtbmc -s z3 -t 20 -i --dump-vcd trace.vcd -m req_ack_good design.smt2

代码获取 ​

两份 RTL（好/坏设计）、sby 配置与完整日志已同步到公开仓库：geek-doc.cn/experiments/sva-assertion-basics-sby。装好 yosys 0.30+ 与 z3 后，按 README 的两段命令即可分别复现 FAILED（含反例 VCD）与 PASSED 两种结果。