极客工场

Appearance

共 2,487 字预计阅读约 8 分钟

Yosys 断言被忽略：用 assert 单元分清读取、综合与验证 ​

更新时间：2026-10-31。本文是开源 EDA 排错系列的 FAQ 速查页，总入口见 开源 EDA 报错排错中心。Yosys 断言被忽略这个说法容易混淆三件事：前端有没有读进属性、综合结果里有没有验证单元、验证工具有没有真正检查属性。这里只讨论第一类与第二类可观察结果；SystemVerilog 其他前端边界可对照 Yosys interface 语法不支持。

本文要回答的问题：Yosys 断言被忽略时查什么 ​

  • 普通 read_verilog -sv 是否必然丢掉 assert？
  • 加上 -formal 后，能证明属性已经通过验证吗？
  • -noassert 对 immediate assertion 和 assert property 的效果一样吗？
  • 为什么有些 concurrent assertion 加 -formal 仍然直接报语法错误？

一、先查属性单元，不要拿退出 0 代替验证结论 ​

assert 是断言：设计要求某个表达式在指定时刻成立。immediate assertion 写在过程块里，随过程执行检查；concurrent assertion 用 assert property 描述属性。两者进入 Yosys 后都可能表现为 $assert 单元，但“单元存在”也只是前端保留了检查意图。

eda/ts-yosys-assertion-ignored.md D2 示意图

读这张图要把绿色与紫色分开：绿色回答“RTLIL 中还有没有 $assert”，紫色回答“属性是否被检查过”。中间多走一步 stat，比凭一条警告标题或一次成功退出猜测可靠。图中的红色只是待核查的问题，不是对任何 Yosys 版本的默认结论。

二、同两份输入跑普通、noassert 与 formal 三种读取 ​

immediate 样例在 valid 为 1 的时钟沿要求 ready 也为 1，同时让寄存器 seen 记录曾经收到请求。下面省略已经确定的端口声明，关键过程保持完整。

systemverilog
always @(posedge clk) begin
    if (valid) begin
        seen <= 1'b1;
        assert (ready);
    end
end

concurrent 样例则放在模块体中，不带时钟和时序蕴含符，只要求 valid 与 ready 相等：

systemverilog
assert property (valid == ready);

六组读取都继续执行 hierarchy -check、proc、check 和 stat。结果不是“普通模式全部忽略”：两种简单断言在普通与 formal 模式下都留下了 1 个 $assert。

这组对照特意保留 -noassert，目的不是推荐关闭检查，而是制造一个可观察的参照：同一份源码只改读取参数，属性和业务单元怎样变化就能直接比较。若只拿普通与 formal 两组相同统计，很容易反过来误以为 -formal 毫无作用；实际上它还负责形式代码分支与相关扩展，只是没有把本文这两条简单属性从 0 个变成 1 个。

统计要在 proc 之后看。前端刚读完时，immediate 断言仍可能藏在过程抽象里；proc 把过程转换为单元后，$assert 才适合作为统一观察点。后续优化或具体器件流程仍可能继续处理这些单元，所以发布网表前还应按实际流程再查一次，而不是把这里的统计当作所有 pass 的永久保证。

输入读取选项退出码$assert 数量本次观察
immediate-sv -noassert00只剩 $dff 与 $mux
immediate-sv01普通读取也保留
immediate-sv -formal01formal 读取保留
concurrent-sv -noassert01本例未被该选项移除
concurrent-sv01生成 $assert 与 $eq
concurrent-sv -formal01与普通读取单元数相同
普通读取的 immediate 断言仍生成 assert 单元

这段输出里 Number of cells: 7 包含 $assert、$dff、$mux，不是“7 个断言”。真正相关的是 $assert 1，末尾 immediate_plain_exit=0 只说明这条读取与转换命令成功。它没有给出任何反例搜索或证明状态。

三、immediate 被移除时，先排查显式 noassert ​

-noassert 的含义就是忽略 assert() 语句。在本文 immediate 样例中，使用它以后退出码仍是 0，但单元从普通读取的 7 个变成 2 个，$assert 消失，过程块原本业务逻辑对应的 $dff 与 $mux 仍在。

exp-log
=== immediate_assert ===
   Number of processes:              0
   Number of cells:                  2
     $dff                            1
     $mux                            1
immediate_noassert_exit=0

所以这次“忽略”没有让命令失败，也没有打印一条足以代替单元统计的错误。若工程脚本、默认参数或包装命令里传了 -noassert，而后续流程需要保留 immediate 断言，正确修正是去掉该选项；准备进入形式验证读取链时，再明确使用 -formal。

但不要机械地给所有综合命令加 -formal。普通读取默认定义 SYNTHESIS，formal 读取改为定义 FORMAL，源文件里的条件编译分支可能因此改变。修复后应同时检查单元统计与功能回归，而不是只看警告是否消失。

四、concurrent 的结果说明选项边界并不整齐 ​

本文的 assert property (valid == ready) 在三种模式下都保留了 $assert，连 -noassert 也没有把它移除。这与 immediate 行形成鲜明对照，说明不能把某个选项对一种断言写法的效果推广到另一种写法。

普通 concurrent 读取最终只有 $assert 和 $eq 两个单元：$eq 计算相等关系，$assert 保存属性检查。formal 模式的统计完全相同，但前端日志由 Parsing SystemVerilog input 变为 Parsing formal SystemVerilog input，这才是本次可直接观察的模式差异。

这也解释了为什么“综合时忽略断言”不能推出“仿真和形式验证同样忽略”。仿真器读取原始 SystemVerilog，有自己的断言执行语义；形式验证需要保留属性并交给相应求解流程。某个综合后端不实现验证单元，不等于另外两条工具链自动失去检查能力。

反过来，仿真没有报错也不能替形式验证背书。测试台可能从未产生 valid=1、ready=0 的激励，immediate 断言便没有遇到失败条件；形式工具则会在给定约束下搜索状态。两种流程回答的问题不同，不能拿一次综合统计或一段无失败的仿真日志替代另一种验证。

工程中还常见条件编译包裹属性：普通读取看到 SYNTHESIS 分支，formal 读取看到 FORMAL 分支。如果 $assert 数量不符合预期，除了命令行选项，还要展开检查宏定义和源码分支。否则即使两种模式都正常运行，读到的也可能根本不是同一段属性代码。

五、formal 不是完整 SVA 语法开关 ​

SystemVerilog Assertions（SVA）是 SystemVerilog 的属性断言机制。另一份输入写成常见的带时钟与蕴含形式：

systemverilog
assert property (@(posedge clk) valid |-> ready);

Yosys 0.33 在普通模式下于 @ 处报 syntax error，加 -formal 仍在同一位置失败。这里的正确处理不是继续堆选项，也不是把语法错误改称为“断言被忽略”，而是确认前端是否接受这类写法，再选择受支持属性表达或合适的形式验证前端。

exp-log
===== clocked_plain =====
concurrent_clocked.sv:6: ERROR: syntax error, unexpected '@'
clocked_plain_exit=1
===== clocked_formal =====
concurrent_clocked.sv:6: ERROR: syntax error, unexpected '@'
clocked_formal_exit=1
result=ordinary-read-versus-formal-read comparison complete
unexpected_failures=0

末尾 unexpected_failures=0 表示脚本观察到了两组预期失败，并不表示时钟属性测试通过。本文只证明这个具体写法在 0.33 的两种读取中被拒绝，不能据此断言所有 SVA 属性都不可用。

六、实际排查按目标保留或移除断言 ​

目标应做的动作不能据此声称的结论
普通综合检查脚本是否主动传 -noassert，确认后端如何处理属性退出 0 就代表属性已验证
保留属性proc; stat 核查 $assert，检查条件编译分支有 $assert 就代表证明通过
形式验证读取使用 read_verilog -sv -formal，再接适配的求解流程-formal 接受全部 SVA
仿真检查在支持相应断言语法的仿真器中运行测试激励综合移除属性会让仿真也忽略

若原日志确实出现忽略断言的 Warning，应保留警告所在阶段和完整读取参数。不同版本、不同属性写法以及后续不同 pass 都可能改变结果；最有效的定位材料是一份最小输入、完整命令和对应的 stat，而不是脱离上下文的半行警告。

代码获取 ​

本文两份受支持断言输入、时钟属性报错输入与八组对照脚本已整理到公开仓：https://github.com/derekzhuo/geek-doc.cn/tree/main/experiments/ts-yosys-assertion-ignored。进入该目录执行 bash run.sh，脚本会复核六组成功转换及两组预期语法失败。

实验环境 ​

  • 机器/系统：Mac / macOS（Darwin 25.5.0，x86_64），Docker 容器运行
  • 工具版本：Yosys 0.33 (git sha1 2584903a060)，镜像 geek-eda:0.2
  • 日期：2026-10-31
  • 完整命令：bash run.sh；脚本以 docker run --rm -v "$PWD:/work" -w /work geek-eda:0.2 yosys ... 执行版本查询和全部对照。本文没有运行仿真或形式求解器，没有给出属性验证通过的结论

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

本篇属于开源 EDA 排错簇的“SystemVerilog 断言读取边界”节点，补充 开源 EDA 报错排错中心 中按前端、转换和验证阶段分流的方法。若问题已经变成接口或 modport 的解析失败，应转到 Yosys interface 语法不支持，不要误用断言选项处理。

总结 ​

Yosys 断言被忽略不能靠综合退出 0 或一句经验判断。Yosys 0.33 实测中，普通 read_verilog -sv 与 -formal 都为本文 immediate 和简单 concurrent 断言生成了 1 个 $assert；-noassert 只移除了 immediate 样例的断言。带 @(posedge clk) 与 |-> 的 concurrent 写法在两种模式下均报语法错误。即便综合阶段不保留或不执行断言，也不代表仿真与形式验证会忽略它；$assert 存在更不等于属性已经验证通过。