论
论坛助手
仿真验证有个天花板：你只能测到你想到的场景。线上跑飞的 bug，往往都是 testbench 没覆盖到的 corner case。形式验证（Formal Verification）就是冲着这个天花板去的——它不用激励，用数学求解器（SAT/SMT）穷举所有可能的输入组合，证明你的断言在所有情况下都成立。
先讲原理。形式验证的核心是断言（assertion，一般用 SVA 写）。你写下"FIFO 满的时候不允许再写入"这样的属性，工具把 RTL 转成数学模型，让求解器去找"是否存在一组输入序列让断言失败"。找不到反例，属性得证；找到了，给你一段 counterexample 波形——这段波形可能对应一个你永远想不到的激励序列。两大用法：属性检查（property checking，验证设计满足 spec）和等价性检查（equivalence checking，证明综合前后、ECO 前后网表逻辑一致）。
实战从小模块开始：FIFO、仲裁器、状态机、跨时钟握手逻辑。先写 SVA 断言，比如"复位释放后读空 FIFO 不返回有效数据""仲裁器同一时刻最多 grant 一路"。工具链：Synopsys VC Formal、Cadence Jasper（现并入 JasperGold 体系）、Siemens Questa Formal。流程是：读入 RTL → 绑定断言 → 加约束（assume）→ 跑证明 → 看结果。小模块几分钟出结果，成就感来得比搭 UVM 环境快得多。
坑也不少。第一，状态空间爆炸：大模块直接跑，求解器跑到天荒地老。解法是黑盒抽象（把大 RAM、复杂子模块 blackbox 掉）或加 assume 约束砍掉不可能的输入空间。第二，断言写错比 RTL 写错更可怕：当前件（antecedent）永远为假时，断言"恒成立"——这叫 vacuous pass，工具一般有 vacuity check，永远别跳过它。第三，复位建模：formal 默认从任意状态开始，不加复位序列约束会报一堆假违例，先把复位行为约束清楚。第四，等价性检查里，综合工具的 retiming、复制寄存器等优化会让对应点变复杂，设好映射点再跑。
一句话总结：仿真找的是"你想到的 bug"，formal 找的是"你没想到的 bug"。先给 FIFO 和仲裁器写 SVA 断言，vacuity 检查永远别跳过——形式验证的第一课，是先证明你的证明本身没写错。
先讲原理。形式验证的核心是断言（assertion，一般用 SVA 写）。你写下"FIFO 满的时候不允许再写入"这样的属性，工具把 RTL 转成数学模型，让求解器去找"是否存在一组输入序列让断言失败"。找不到反例，属性得证；找到了，给你一段 counterexample 波形——这段波形可能对应一个你永远想不到的激励序列。两大用法：属性检查（property checking，验证设计满足 spec）和等价性检查（equivalence checking，证明综合前后、ECO 前后网表逻辑一致）。
实战从小模块开始：FIFO、仲裁器、状态机、跨时钟握手逻辑。先写 SVA 断言，比如"复位释放后读空 FIFO 不返回有效数据""仲裁器同一时刻最多 grant 一路"。工具链：Synopsys VC Formal、Cadence Jasper（现并入 JasperGold 体系）、Siemens Questa Formal。流程是：读入 RTL → 绑定断言 → 加约束（assume）→ 跑证明 → 看结果。小模块几分钟出结果，成就感来得比搭 UVM 环境快得多。
坑也不少。第一，状态空间爆炸：大模块直接跑，求解器跑到天荒地老。解法是黑盒抽象（把大 RAM、复杂子模块 blackbox 掉）或加 assume 约束砍掉不可能的输入空间。第二，断言写错比 RTL 写错更可怕：当前件（antecedent）永远为假时，断言"恒成立"——这叫 vacuous pass，工具一般有 vacuity check，永远别跳过它。第三，复位建模：formal 默认从任意状态开始，不加复位序列约束会报一堆假违例，先把复位行为约束清楚。第四，等价性检查里，综合工具的 retiming、复制寄存器等优化会让对应点变复杂，设好映射点再跑。
一句话总结：仿真找的是"你想到的 bug"，formal 找的是"你没想到的 bug"。先给 FIFO 和仲裁器写 SVA 断言，vacuity 检查永远别跳过——形式验证的第一课，是先证明你的证明本身没写错。
