极客工场

Appearance

共 2,631 字预计阅读约 9 分钟

Verilator 断言开启流程：--assert 开关、SVA 子集与失败退出码实测 ​

更新时间：2026-11-03。断言（assertion）是写在 RTL 里的「设计自带检查器」：约定满 FIFO 不能再写、复位后状态必须清零，仿真时一旦违例就当场报错。SystemVerilog Assertion 断言模板 给了可复制的性质写法，但那篇默认你用的是商业仿真器；本篇解决 Verilator 这条开源链路上的具体问题——断言要怎么编译进去、哪些 SVA 语法在 5.020 真的能过、失败后进程是什么下场。Verilator 与 VCS 的整体差异可先读 Verilator 与 VCS 的主要差异。

本文要回答的问题 ​

  • Verilator 里断言为什么默认不生效，--assert 开关到底改变了什么？
  • immediate assert 和 concurrent assert property 在 Verilator 5.020 分别能写到什么程度？
  • 完整的开启命令怎么拼，每个参数不加会怎样？
  • 断言失败时真实输出和退出码是什么，能不能直接交给 CI 判定？
  • 哪些 SVA 语法在编译期就被拒绝，需要改写或换工具？

一、这一步在流程里的位置 ​

断言检查发生在「编译仿真」这一步内部，不产生新的交付文件，只决定最终可执行文件里有没有检查逻辑。上游是带 assert 的 RTL 和 C++ harness，下游是一个「违例即中止」的仿真程序，可以直接挂进回归脚本，靠退出码判定通过与否。

eda/flow-verilator-assert.md D2 示意图

读这张图抓住一条分叉：同一份 RTL、同一个 harness，唯一变量是有没有 --assert。加了开关，违例在发生当拍就把进程打死；不加，第五拍的满写照样发生、仿真照样退出 0，看起来一切正常——这是最危险的情况。

断言在 SVA 里分两种形态，Verilator 的支持度并不相同，先把边界钉死：

形态写法特征Verilator 5.020 实测对照 VCS
immediate assert过程块内 assert(条件) else $error(...)，当拍立即求值完整支持，需 --assert 编译完整支持
concurrent assert（单拍采样）assert property (@(posedge clk) disable iff (...) 性质)支持采样值、`=>、$stable、$onehot0` 等
concurrent assert（多拍序列）含 ##1、##[1:3] 延迟或命名 sequence编译期 %Error-UNSUPPORTED 拒绝完整支持

本篇 RTL 用最稳的 immediate assert；concurrent 的可过写法见断言模板篇，越界写法在第五节有真实编译报错。

Verilator 断言开启：一个开关、两种断言、一条子集边界

这张卡对应全文的四个抓手：开关决定有没有检查，immediate 与单拍 concurrent 是可用区，## 时序序列是不可用区。选型时优先用 immediate assert 表达「这一拍不许发生」，把跨拍性质留给支持完整 SVA 的工具或改写为状态机检查。

二、命令逐段解读 ​

实验对象是一个深度 4、位宽 8 的同步 FIFO（FIFO 与仲裁器基础 讲过指针与空满逻辑）。构建违规版本的完整命令分两步：

bash
verilator --cc --exe --assert -Wno-fatal --top-module fifo \
  -Mdir build_bad fifo.sv tb_bad.cpp
make -C build_bad -f Vfifo.mk -j2
  • --cc：只把 RTL 翻译成 C++ 并生成 Makefile，不自动调 g++；配合手写 C++ harness 时用它，产物编排最可控（图省事可换 --binary 让翻译、生成 main、编译一条命令完成，但多构建并存的实验场景下 --cc 加独立 -Mdir 更清晰）。
  • --exe：声明后面的 tb_bad.cpp 是测试台。不加它，Verilator 会自动生成一个自己的 main，链接时与 harness 的 main 冲突，报 multiple definition of 'main'。
  • --assert：本篇主角。它让 Verilator 保留 RTL 中的断言检查并生成失败处理代码；不加时所有 assert 在翻译阶段被剔除，第五节有对照实测。
  • -Wno-fatal：lint 告警只打印不中止。教学代码难免有风格告警，先让仿真跑起来；正式工程应按 Verilator lint 高频告警矩阵 逐条清，再考虑去掉这个降级开关。
  • --top-module fifo：显式指定顶层，多文件工程里不写可能选错顶层。
  • -Mdir build_bad：生成代码与二进制的目录。实验里要并存三个构建（无断言、违规、修复），用不同目录隔开；目录需预先存在，且只建议用单层目录名，二级嵌套会让生成的 Makefile 找不到相对路径的源文件。
  • make -C build_bad -f Vfifo.mk：第二步编译。-f Vfifo.mk 的名字跟顶层模块走（顶层叫 fifo 就是 Vfifo.mk），-j2 并行编两个 g++ 任务。

RTL 里的断言写在时序逻辑块内，与指针更新并列，失败动作用 $error 打印带现场的消息：

systemverilog
a_no_overflow: assert (!(wr_en && full && !rd_en))
  else $error("FIFO overflow: write while full, count=%0d", count);
a_no_underflow: assert (!(rd_en && empty && !wr_en))
  else $error("FIFO underflow: read while empty, count=%0d", count);

注意满时同拍一读一写是合法的（数据原地轮换），所以条件是「满且只写不读」，不能图省事写成 !(wr_en && full)，否则合法流量会被误杀。

三、输入输出文件 ​

阶段吃进去吐出来
verilatefifo.sv（含 2 条 assert）、tb_bad.cpp、命令行开关build_bad/ 下的 Vfifo.mk、Vfifo.cpp、Vfifo__main.cpp 被排除（harness 提供 main）
make上面的 C++ 与 Verilator 运行库build_bad/Vfifo 原生可执行文件
运行harness 产生的时钟与激励终端检查信息；失败时进程以信号中止

harness 是 C++，每个时钟步把输入摆好、翻两次 clk、各调一次 eval()。违规 harness 无视 full 标志连续写 5 拍，容量只有 4，第 5 拍必然踩线：

cpp
d->wr_en = 1; d->rd_en = 0; d->din = (unsigned char)(0xA1 + i);
d->clk = 0; d->eval();
d->clk = 1; d->eval();   // 第 5 个上升沿：full=1 且仍在写

四、常见错与检查点 ​

现象先查什么纠正
故意写了违例激励，仿真却退出 0verilate 命令有没有 --assert开关漏了，断言被整体剔除；这不是断言写错，是根本没编进去
编译报 %Error-UNSUPPORTED: ## (in sequence expression)assert property 里是否用了 ## 延迟或命名 sequence把多拍性质改写成 immediate assert 加状态寄存器，或交给 VCS 这类完整 SVA 仿真器
链接报 multiple definition of 'main'是否漏了 --exe加 --exe，让 Verilator 放弃自带 main
修复版弹出的数据全部错位一拍是否在上升沿之后才读组合输出 dout组合读数据在 clk 低相（沿前）采样；沿后读指针已经推进，拿到的是下一项

一个口径要点：Verilator 的断言失败不是「打印一行继续跑」。默认失败动作等价 $stop，进程收到中止信号直接结束，shell 里看到的退出码是 134（128 + SIGABRT 的信号编号 6）。这意味着它天然适配 CI：非零即失败，不需要自己 grep 日志。

五、真实跑一遍：违规被拦、修复跑净、越界语法被拒 ​

在 geek-eda:0.3-sta 容器（Verilator 5.020）里，同一 FIFO 与 harness 跑三轮。第一轮故意不加 --assert：5 拍写入全部完成，BAD TB FINISHED 都打出来了，退出码却是 0——检查完全缺席。第二轮加上 --assert，第 5 拍（仿真时刻 70）断言当场触发：

加 --assert 后第 5 拍满写：断言触发，退出码 134

报错行信息很完整：fifo.sv:32 定位到 a_no_overflow 的源行，层次路径 TOP.fifo.a_no_overflow 指明是哪条断言，$error 文本带出现场 count=4。排查时直接按源行和违例时的计数往回查激励，不用猜。

第三轮把 harness 改成尊重 full 反压：写满 4 项后读空、逐拍核对读出顺序，再写一批验证指针回绕。断言全开的同一个可执行文件上复跑，违例不再出现，记分板打印通过：

修复 harness 后断言全开复跑：两批读写零违例

pop 1 到 pop 4 的 0x10–0x13 说明读出顺序与写入一致，第二批读完 empty=1，最终 RESULT: PASS、退出码 0。修复的不是 RTL——RTL 的保护一直都在——而是激励对反压的尊重；断言的价值正是让「上游不守规矩」在仿真阶段就暴露，而不是等到上板数据错乱。

最后实测子集边界。把性质写成「req 之后隔一拍 ack」的多拍序列，Verilator 在编译期直接拒绝，不生成任何 C++：

exp-log
%Error-UNSUPPORTED: sva_subset_delay.sv:6:59: Unsupported: ## () cycle delay range expression
    6 |   a_req_then_ack: assert property (@(posedge clk) req |=> ##1 ack)
      |                                                           ^~
%Error-UNSUPPORTED: sva_subset_delay.sv:6:63: Unsupported: ## (in sequence expression)
%Error: Exiting due to 2 error(s)

这是「明确不支持」而非「悄悄忽略」，行为是安全的：看到 UNSUPPORTED 就该改设计验证策略，immediate assert 配合几个状态位足以覆盖「N 拍内必须应答」这类常见检查；真正重度的 SVA 序列库仍应放在 VCS 等完整仿真器或形式验证工具里跑。

实验环境 ​

  • 机器/系统：macOS（Darwin 25.5，Apple Silicon）上 Docker Desktop，容器镜像 geek-eda:0.3-sta（Debian bookworm 系）
  • 工具版本：Verilator 5.020 2024-01-01 rev (Debian 5.020-1)，容器内 g++ (Debian 12.2.0) + GNU make（verilator -V 首行照抄）
  • 日期：2026-11-03
  • 完整命令：bash run.sh 起容器执行 run-native.sh，内部依次为三轮 verilator --cc --exe [--assert] -Wno-fatal --top-module fifo -Mdir build_<名> fifo.sv tb_*.cpp + make -C build_<名> -f Vfifo.mk -j2 + 运行可执行文件并记录退出码，附录一轮 verilator --lint-only --assert sva_subset_delay.sv

代码获取 ​

完整 RTL、两份 C++ harness、SVA 子集探针、Makefile 与容器复现脚本已同步到公开仓库：geek-doc.cn/experiments/flow-verilator-assert，克隆后进入该目录执行 make run（需要 Docker 与 geek-eda:0.3-sta 镜像）即可复现三轮对照与编译期拒绝输出，本机已装 Verilator 5.x 时用 make NATIVE=1 run，make clean 删除全部构建目录。

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

总结 ​

Verilator 断言开启流程一句话：RTL 里写 immediate assert，verilate 时务必加 --assert（配合 --cc --exe 与 C++ harness），断言失败会在违例当拍中止仿真、退出码 134，干净跑完为 0，可直接进 CI。5.020 支持 immediate assert 与单拍采样的 assert property，但 ## 多拍序列和命名 sequence 编译期即报 %Error-UNSUPPORTED；忘了开关时断言被静默剔除，是这条流程上唯一会让你「带着空检查器上路」的坑。