Yosys check 检查流程：综合前置门禁的位置、选项与 check -assert 用法
更新时间：2026-11-03。开源 EDA 工具链里，综合是什么 讲过 RTL 要先翻译成通用网表再做优化与映射。Yosys 在这条流水线里内置了一个结构性体检 pass——
check。本篇讲它在正常流程里的位置和用法：什么时候放、查什么、不查什么、怎么用check -assert把它接成 CI 门禁。单条问题的排错请看 多驱动警告排查，工具链全貌见 开源 EDA 工具链。
本文要回答的问题
check应该插在综合脚本的哪两个 pass 之间，放早了会怎样？- 它到底查哪些问题，
-assert、-mapped这些选项各自什么场景用？ - 为什么位宽截断这种错误
check一个字都不报？ - 怎么把
check -assert写成非零退出的门禁，让坏设计进不了后续流程？
一次最小流程只有三拍，先给总览：
读这张卡抓住一条主线：第三拍把「体检」和「否决」合在一站——check 负责喊话，-assert 负责关门，流水过了它才允许进入优化与工艺映射；闸门本身不改设计。
一、这一步在综合流程里的位置
上游给 check 的是经过 proc 翻译的通用网表：read_verilog 负责解析精化，hierarchy -top 选定顶层并把例化层次连起来，proc 把 always 块翻译成触发器、多路器这类内部 cell。check 体检通过后，下游才是 opt、techmap 以及 synth_* 脚本里的工艺映射。数据流如下：
图里红色的 check 是唯一带否决权的一站。注意它在 proc 之后：多驱动这类问题发生在 cell 与连线层面，always 块还躺在过程块描述里时，网表层面的打架是看不见的——放早了会得到假的零问题，第四节用实测证明。
二、check 命令逐段解读
Yosys 0.33 的 check 语法是 check [options] [selection]，不带选择时检查当前设计的全部模块。它只查三件事（yosys -h check 原文）：组合逻辑环（combinatorial loops）、一张网有两个以上互相冲突的驱动源、被使用但没有驱动源的线网。选项如下：
| 选项 | 作用 | 不加会怎样 |
|---|---|---|
-assert | 发现任何问题就抛 runtime error、以退出码 1 中止 | 只打 Warning，脚本照样往下跑，坏设计流进后端 |
-mapped | 额外检查是否还有未映射到目标工艺的内部 cell | 只查前述三类结构问题，漏网的未映射 cell 留给后续 pass 暴露 |
-allow-tbuf | 修改 -mapped 行为，允许保留三态缓冲 $_TBUF_ | 配合 -mapped 时三态总线会被当成未映射问题报出 |
-noinit | 额外检查带 init 属性的线网 | 初始值风格问题不提示 |
-initdrv | 检查带 init 属性却不由触发器驱动的线网 | 同上，更窄的一条初始值规则 |
生产脚本里 90% 的情况只需要 check -assert 这一个开关。-mapped 用在工艺映射之后做二次体检（确认通用 cell 已全部落库），本篇的前置门禁用不到；-noinit/-initdrv 是团队对复位风格有硬性规定时才打开。
三、输入输出文件：吃什么、吐什么
check 不产生文件，它的输入是内存中的当前设计，输出是终端上的 CHECK pass 段落。工程上通常把命令序列写进 .ys 脚本（Yosys 原生脚本格式，一行一条 pass），例如本篇的门禁脚本 gate.ys：
read_verilog alu.v
hierarchy -top alu
proc
check -assert执行方式是 yosys gate.ys；临时验证也可以用一行 -p 串起来，如 yosys -p 'read_verilog alu.v; hierarchy -top alu; proc; check -assert'，工程固定后把序列沉淀进 .ys 文件更利于版本管理与回归。干净时它打印 Found and reported 0 problems. 并以退出码 0 收尾；有问题时先逐条列 Warning，最后一行 ERROR: Found N problems in 'check -assert'.，退出码 1。Makefile 或 CI 里不用解析日志，直接看 $? 即可决定是否中断。
check 还可以带选择参数，只检查某个模块或某层层次（语法见 yosys -h select），大工程里想把问题隔离到新增模块时有用；小设计直接全量检查即可。
四、常见错与检查点
| 现象 | 先查什么 | 纠正 |
|---|---|---|
| 明明有两个 always 块驱动同一信号，check 却报 0 problems | check 是否放在了 proc 之前 | 把顺序固定为 hierarchy -top; proc; check，过程块翻译后再体检 |
| 位宽截断、溢出 bug 一个警告都没有 | 没找错地方——check 只查结构三类，本就不查位宽 | 位宽问题交给独立 lint，见 位宽不匹配警告 与 SpyGlass RTL Lint 实战 |
| 日志全是 Warning 但脚本继续跑、网表照出 | 是否漏了 -assert | 门禁脚本一律写 check -assert，用退出码拦截 |
| 报 combinatorial loop | 组合赋值是否成环（a 依赖 b、b 又依赖 a） | 定位与打断环路的完整过程见 check 组合环报错 |
最需要记住的是第二条的边界：check 不是 lint。它关心的是「这张网表物理上成不成立」——两根输出短接（多驱动）、信号悬空没人驱动（无驱动）、组合逻辑首尾相连（组合环）；至于赋值两侧位宽是否一致、敏感表漏没漏信号、case 有没有 default，属于编码规则与行为正确性，要靠 Verilator -Wall 或商业 lint 工具另设一道防线。
五、真实跑一遍：埋错、被抓、门禁拦截、修复归零
用一个 4 位 ALU 小设计做对照。坏版本 alu_bad.v 故意埋了两处：y 同时被一个时序 always 块和一个组合 always 块赋值（多驱动）；b 是 5 位、a+b 的和却塞进 4 位的 sum（位宽截断）。先验证「放早了假清净」——read_verilog; hierarchy; check（无 proc）的输出是 Found and reported 0 problems.。补上 proc 后再 check，真实输出如下：
读这段输出：警告按位展开，4 位网各一条。被报的网叫 $add$alu_bad.v:14$1_Y 而不是 y，是因为 proc 把组合块的 y = sum 提升成了直连、把 y 与加法器输出合并成了同一张网；于是这张网上同时挂着时序块综合出的触发器（$procdff$7 的 Q 端）和加法器（$add 的 Y 端），两个驱动源在缩进两行里写得明明白白。而位宽截断那条——如第四节所料——check 一言不发。
接着让坏设计过 check -assert 门禁脚本，Warning 之后被一行 ERROR 终止，退出码为 1：
ERROR: Found 4 problems in 'check -assert'.
gate-bad exit code = 1修复版 alu.v 把两个 always 块合并成一个时序块、用 en 在块内做选择，位宽改为 a、b 均 4 位、和放进 5 位的 sum。同一套脚本复跑，CHECK pass 与门禁退出码如下：
4. Executing CHECK pass (checking for obvious problems).
Checking module alu...
Found and reported 0 problems.
gate exit code = 0零问题加退出码 0，门禁放行，设计才允许进入后面的 opt 与映射。多驱动单条问题的深入排查见 Yosys multiple drivers 警告，无驱动类警告见 undriven 警告排查。
实验环境
- 机器/系统：Mac mini（Apple Silicon，macOS 15），docker 容器内运行
- 工具版本：Yosys 0.33（git sha1 2584903a060），镜像 geek-eda:0.3-sta
- 日期：2026-11-03
- 完整命令序列：
yosys -V→yosys -p 'read_verilog alu_bad.v; hierarchy -top alu_bad; check'（proc 之前，假清净）→yosys -p 'read_verilog alu_bad.v; hierarchy -top alu_bad; proc; check'（4 条多驱动）→yosys gate-bad.ys（check -assert，退出码 1）→yosys -p 'read_verilog alu.v; hierarchy -top alu; proc; check'与yosys gate.ys（0 problems，退出码 0）
代码获取
完整对照工程（alu_bad.v、alu.v、gate.ys、gate-bad.ys、run.sh 与 Makefile）见公开仓库 geek-doc.cn/experiments/flow-yosys-check-command；装好 Docker 后执行 make run 即按 STEP A–E 顺序复现假清净、警告、门禁失败与修复归零的完整过程，本机原生装有 Yosys 时可用 make native。
这一篇在知识体系里的位置
- 想理解 check 之前各 pass 在干什么：读 综合是什么 与 逻辑综合上手；
- check 报出的单条问题怎么逐条排查：多驱动见 multiple drivers 警告，组合环见 check 组合环报错，无驱动见 undriven 警告；
- check 管不到的位宽与编码规则：读 位宽不匹配警告 与 SpyGlass RTL Lint 实战；
- 开源工具链里这一步的上下游：见 开源 EDA 工具链 与 报错排查总览。
总结
Yosys check 检查流程的标准位置是 read_verilog; hierarchy -top; proc 之后、优化与映射之前：它只对翻译后的网表做体检，查多驱动、无驱动、组合环三类结构错误，放在 proc 之前会得到假清净；check 不是 lint，位宽截断与编码规则要另靠 Verilator 或 SpyGlass；正常写法是把 check -assert 放进 .ys 门禁脚本，有问题即 ERROR 加退出码 1、干净则 0 problems 放行——埋错的 4 位 ALU 实测完整演示了警告按位列出驱动源、门禁拦截、合并驱动块并修正位宽后复跑归零的全过程。