SpyGlass lint 断言与 bind 不生效：层级、实例名、复位初态与编译开关速查
更新时间：2026-10-24。FAQ 速查页，属于 EDA 工具排错系列，总入口见 开源 EDA 报错排错中心。SpyGlass 跑断言相关 goal（如
lint/lint_rtl附带 SVA 检查，或专门的 assertion 结构检查）时，常见翻车不是断言逻辑写错，而是断言根本没挂上去：bind 语句找不到目标实例、checker 文件没进 filelist、断言编译开关没开，工具静默跳过，报告里一条都没有——你以为「零违例」很干净，其实是「零检查」。本篇处理这类「断言/bind 不生效」的排查。它和 SpyGlass lint 引用无法解析速查 的分界是：那篇查引用绑定硬错误（有 Error），本篇查「没有任何报错但断言没生效」的静默失效。
本文要回答的问题
- 报告里一条断言违例都没有，怎么判断是「真干净」还是「根本没挂上」？
- bind 语句的目标层级、实例名写错时，SpyGlass 给什么提示？
- 断言编译开关（SVA 相关 option）没开会怎样？日志哪里能确认断言被读进来了？
- 复位期间 X 初态导致断言误触发或永不触发，怎么隔离？
一、报错原文与典型现象
这类问题最典型的形态是没有报错——goal 跑完 0 violation，但统计信息里断言计数为 0。其余可见提示如下（工程路径均为占位）：
1. bind 目标找不到：
Warning: [demo_bind.sv:12]: bind target instance 'demo_top.u_core.u_fifo' not found; bind statement ignored.
Warning: Bind of checker 'fifo_sva' to 'demo_fifo' matched 0 instances.2. 断言编译被跳过：
Info: Assertion compilation is disabled (set_option enable_assertion no); SVA constructs ignored.
Warning: [demo_fifo.sv:88]: 'assert property' ignored: assertion support not enabled for this goal.3. 复位初态引发的异常触发：
Warning: Assertion 'a_req_ack' fails at time 0 (X on reset or uninitialized sampling).
Info: 3 assertions vacuously pass throughout (antecedent never true).判据一句话：先查断言计数——goal 报告或 spyglass.log 里搜 assertion 统计，计数为 0 就是没挂上；计数正常但结果异常（time 0 全挂、全程 vacuous）才进初态与逻辑分支。最容易被忽视的是「半挂上」状态：bind 成功了一部分实例、另一部分静默跳过，计数比预期少但不归零——所以计数要和设计里的预期清单对账，而不是只看是不是零。
二、病因处置速查表
| 现象 | 可能原因 | 处置 |
|---|---|---|
| 断言计数为 0 | SVA 支持未开：缺 set_option enable_assertion yes 或语言标准不含 SVA | .prj 开断言选项，核 set_option language sverilog |
| bind matched 0 instances | 目标层级路径或实例名写错、目标被宏裁掉 | 按编译后层级树逐级核对路径；确认 `ifdef 段状态 |
| bind target not found | bind 指向的模块被 inline 或层级打平 | 保层级（preserve_hierarchy）或改 bind 到打平后路径 |
| checker 文件未生效 | checker/bind 文件没进 filelist 或排在目标之前顺序不对 | filelist 补入；bind 文件随 checker 一起编译 |
| 断言全 vacuous pass | 前提条件（antecedent）永假：采样信号常量、门控时钟不翻 | 查激励与门控；确认不是参数裁剪成常量 |
| time 0 即 fail | 复位未释放前 X 初态参与采样 | 断言加 disable iff (rst)，确认复位极性与释放时刻 |
| 复位期误触发一批 | 断言没写 disable iff，或复位名接错 | 补 disable iff；核对 bind 端口映射里的复位连接 |
| bind 端口连不上 | checker 端口与目标信号宽度/方向不匹配 | 核 bind 端口映射表，宽度不匹配会静默丢弃或告警 |
| 同一 checker 部分实例生效 | bind 用模块名但部分实例被参数裁剪 | 按实例名 bind，或核对 generate 裁剪范围 |
| 改过 bind 后计数不变 | work/ 增量库沿用旧编译 | 清 work/ 全量重跑再查计数 |
三、排查决策图
下面这张图按「断言现在处于什么状态」分流：红色是现象入口，三个蓝色判定依次问「编译进没进来、bind 挂没挂上、挂上后行为对不对」，橙色处理增量缓存假象，绿色统一复验，紫色把检查固化成纪律。
读这张图抓一条主线：永远先看计数再看结果。零违例只有在「断言计数等于预期」的前提下才是好消息；计数不对，一切结果都没有意义。
四、逐条排查展开
第一步：确认断言真的被编译进来。 SpyGlass 默认不一定启用 SVA：.prj 里要有 set_option enable_assertion yes（具体选项名以所用版本文档为准），且 set_option language sverilog 保证 assert property 等构造被识别。验证方法不是看选项写了没有，而是看日志——编译摘要里应有 assertion 统计行，goal 报告里应列出发现的断言清单。计数为 0 就停在第 一步，别往下查逻辑。顺手再核一遍 filelist：checker 与 bind 文件漏列时不会报「文件找不到」级别的错，只是断言构造根本没进编译单元，表现与开关没开完全一样，两者要一起排除。
第二步：bind 挂接核对层级与实例名。 bind 语句的目标是编译后的层级路径，常见三类错：路径里某级实例被 `ifdef 裁掉（宏没传时 generate 段不存在）；目标模块被 inline、层级打平后路径少了一截；实例名大小写或数组下标写错。核对方法是在 GUI 层级树里逐级展开到目标实例，把实际路径抄进 bind。bind 到模块名（所有实例）却只想覆盖部分实例时，改用实例路径 bind；checker 端口映射要逐位核对宽度，宽度不匹配有的版本只给一条不起眼的 Warning，端口实际悬空。还有一种隐蔽失效：bind 语句本身编译通过了，但它所在的文件排在目标模块之后、或bind 目标在当前 goal 的裁剪范围外（例如只 lint 某个子系统），bind 照样 matched 0——这时要核 goal 的读入范围与 read_file 覆盖，而不是改 bind 语法。
第三步：挂上了再查行为——vacuous 与 time 0 两类异常。 全程 vacuous pass 说明前提条件从未为真：顺着 antecedent 里的信号往上找，常见是门控时钟不翻、使能被参数 tie 成常量、或者激励根本没到（静态检查里激励概念换成「状态可达性」，但常量前提同样让断言形同虚设）。time 0 即 fail 或复位期一批误触发，多半是 X 初态参与了采样——规矩写法是每条断言带 disable iff (!rst_n)，复位名与极性在 bind 端口映射里接对；复位连接错了，断言在复位期照样采样，报出来的全是无效违例。排查这两类异常时先分类再动手：vacuous 是「前提死了」，查常量与可达性；time 0 即挂是「初态脏了」，查复位与 disable iff——两类病因完全不同，混着改容易越改越乱。
第四步：清缓存复验。 bind 关系与断言编译结果都缓存在 work/ 增量库，改过 bind 文件、checker 或 option 之后必须删 work/ 全量重跑，再核对断言计数。配置解析层面的前置失败（.prj 写错导致 option 没生效）可对照 SpyGlass 工程配置解析失败速查；层级被优化打平导致的 bind 失效，与 SpyGlass lint 信号被优化看不到速查 同根，处理手法互通。
五、规范做法与预防
- 断言计数进回归基线：每次回归核对断言总数与 bind 成功数，计数掉了就当红灯处理，杜绝「静默零检查」。
- bind 文件与 checker 同目录同 filelist 段：bind 语句紧贴 checker 编译，目标路径变更时一起改，评审时成对看。
- 每条断言强制 disable iff：复位名、极性写成工程模板，新断言照抄模板，不允许裸 assert 入库。
- 层级稳定优先：bind 目标所在层级加保留配置，避免优化级别变化时 bind 路径整体失效。
- 改 bind/checker/option 后清
work/：作为 checklist 固定项，不靠增量结果下结论。 - 预期断言清单对账：每个子系统维护一份「应生效断言清单」（checker 名、目标实例数、预期计数），回归后逐项核对，半挂上状态也能第一时间暴露。
这一篇在知识体系里的位置
本篇是 EDA 排错速查簇的一员，总入口见 开源 EDA 报错排错中心。层级被优化导致 bind 目标消失见 SpyGlass lint 信号被优化看不到速查，option 未生效的配置层面排查见 SpyGlass 工程配置解析失败速查，编译期绑定硬错误见 SpyGlass lint 引用无法解析速查；规则体系整体定位见 RTL 静态检查（Lint）：SpyGlass 规则体系与基线门禁。
一句话总结
SpyGlass lint 断言不生效的典型形态是「静默零检查」：先看断言计数确认编译开关与语言标准，再按编译后层级树核对 bind 路径与实例名（警惕 ifdef 裁剪与层级打平），挂上之后用 disable iff 收复位初态、用激励/常量分析收 vacuous；改完清 work/ 全量重跑，并把断言计数纳入回归基线——零违例只有配上正确的计数才算数。