开源 FPGA 03｜形式验证入门：SymbiYosys + SMT 证明你的 RTL 永不出错

 ___ ___  ___ __  __   _   _
| __/ _ \| _ \  \/  | /_\ | |
| _| (_) |   / |\/| |/ _ \| |__
|_| \___/|_|_\_|  |_/_/ \_\____|

 __   _____ ___ ___ ___ ___ ___ _____ ___ ___  _  _
 \ \ / / __| _ \_ _| __|_ _/ __|_   _|_ _/ _ \| \| |
  \ V /| _||   /| || _| | | (__  | |  | | (_) | .` |
   \_/ |___|_|_\___|_| |___\___| |_| |___\___/|_|\_|

   开源 FPGA 实战系列 · 第 03 篇
   用数学证明代替运气测试

系列第 3 篇 · 工具：SymbiYosys 0.40 · Bitwuzla 0.5 · Z3 4.12 上一篇：时序收敛实战

0. 这一篇要解决什么问题

你写了一个 FIFO，测了一百万个随机输入，没有发现 overflow。你有多大把握它是正确的？

答案：不知道。 随机测试的覆盖率永远不是 100%。也许那个触发 overflow 的状态序列需要 2^32 步才能到达。

形式验证（Formal Verification）换了一种思路：

不测试，而是证明。 “对于所有可能的输入序列和初始状态，这个 FIFO 永远不会 overflow。”

这不是”测了很多次”，这是数学证明。

本篇目标：

理解形式验证的数学基础（不需要会写证明，只需要理解思路）
安装 SymbiYosys 工具链
用 assert / assume / cover 写属性
对 FIFO 进行 BMC 和 Induction 证明
解读 SymbiYosys 生成的反例 VCD

本篇不覆盖：

等价性检查（Equivalence Checking）
属性规范语言（PSL / SVA 完整语法）
工业级形式验证平台（Cadence JasperGold 等）

1. 形式验证 vs 仿真：本质区别

仿真只能采样测到极小部分状态空间；形式验证用 SMT 求解器穷举所有可达状态来证明属性恒成立。

1.1 SMT 求解器的角色

SymbiYosys 的工作流程：

你的 RTL（Verilog）+ 属性（assert/assume/cover）
           ↓  Yosys 展开成逻辑网表
SMT-LIB 2 格式的布尔满足性问题
           ↓  SMT 求解器（Bitwuzla / Z3）求解
结论：
  - UNSAT（不可满足）→ 属性永远成立（PROOF）
  - SAT（可满足）    → 找到了反例（COUNTEREXAMPLE）

SMT（Satisfiability Modulo Theories）是”带背景理论的可满足性”，支持位向量、数组等。比纯 SAT 求解器更擅长处理硬件设计。

1.2 速度对比

方法	找到 FIFO overflow bug 的时间
随机仿真（iverilog）	永远找不到（概率约 1/2^20）
覆盖率驱动仿真	数小时到数天
BMC（SymbiYosys）	2-10 秒
Induction 证明	5-60 秒

2. 安装 SymbiYosys

2.1 通过 OSS CAD Suite（最简单）

# OSS CAD Suite 已经包含 sby + bitwuzla + z3 + yosys
source oss-cad-suite/environment

sby --version    # SymbiYosys 0.40
bitwuzla --version  # Bitwuzla 0.5.0
z3 --version     # Z3 version 4.12.4

2.2 手动安装（Ubuntu 22.04）

# 安装依赖
sudo apt install -y python3 python3-pip build-essential \
    cmake git yosys

# 安装 SymbiYosys
pip3 install symbiyosys

# 安装 Bitwuzla（推荐，比 Z3 快 2-5 倍用于硬件验证）
# 从源码编译
git clone https://github.com/bitwuzla/bitwuzla.git
cd bitwuzla
./configure.py --prefix ~/.local
cd build && make -j$(nproc) && make install

# 验证
sby --version        # SymbiYosys 0.40
~/.local/bin/bitwuzla --version  # Bitwuzla 0.5.0

2.3 工具依赖关系

SymbiYosys (sby)
    ├── Yosys         ← RTL 综合 + 展开
    ├── Bitwuzla      ← SMT 求解器（推荐，速度快）
    ├── Z3            ← 备用 SMT 求解器
    ├── Boolector     ← 另一个 SMT 求解器
    └── iverilog/verilator  ← 用于 cover 模式仿真验证

3. assert / assume / cover 语法

3.1 三个核心原语

// 在 SystemVerilog 中使用属性

// assert：你声明"这个条件必须永远成立"
// SymbiYosys 会尝试找到让它为 false 的输入序列
assert property (@(posedge clk) fifo_count <= DEPTH);

// assume：你告诉工具"输入只会满足这些条件"
// 限制搜索空间（约束输入）
assume property (@(posedge clk) !(push && pop && fifo_empty));

// cover：你要求工具找到一条能让条件成立的路径
// 用于验证"这个状态是可达的"
cover property (@(posedge clk) fifo_full && push);

3.2 Clocking 和 Reset 的写法

// 形式验证通常需要明确的初始状态约束
// 在 module 内部添加：

`ifdef FORMAL

// 跟踪是否已经经历过至少一个时钟周期（避免初始状态误报）
reg f_past_valid = 1'b0;
always @(posedge clk) f_past_valid <= 1'b1;

// 用 $past() 函数访问上一个时钟的值
// 例如：如果上个周期 push 有效，这个周期 count 应该增加
always @(posedge clk) begin
    if (f_past_valid && $past(push) && !$past(full))
        assert(count == $past(count) + 1);
end

`endif

4. 完整示例：证明 FIFO 永远不会 Overflow

4.1 FIFO 实现（含形式验证属性）

// sync_fifo.sv
// 同步 FIFO，支持形式验证
// 参数：DEPTH=8（2的幂），DATA_WIDTH=8

module sync_fifo #(
    parameter DATA_WIDTH = 8,
    parameter DEPTH      = 8,            // 必须是 2 的幂
    parameter ADDR_BITS  = $clog2(DEPTH) // = 3 for DEPTH=8
) (
    input  wire                  clk,
    input  wire                  rst_n,
    // 写端口
    input  wire                  push,        // 写请求
    input  wire [DATA_WIDTH-1:0] wdata,       // 写数据
    output wire                  full,        // FIFO 满
    // 读端口
    input  wire                  pop,         // 读请求
    output reg  [DATA_WIDTH-1:0] rdata,       // 读数据
    output wire                  empty,       // FIFO 空
    // 状态
    output wire [ADDR_BITS:0]    count        // 当前元素数量
);

    // ── 存储体 ──
    reg [DATA_WIDTH-1:0] mem [0:DEPTH-1];

    // ── 指针（多一位用于空/满判断）──
    reg [ADDR_BITS:0] wr_ptr;  // 写指针（ADDR_BITS+1 位）
    reg [ADDR_BITS:0] rd_ptr;  // 读指针（ADDR_BITS+1 位）

    // ── 空/满判断 ──
    // 技巧：用最高位区分空和满
    // 相同低位 + 相同高位 → 空
    // 相同低位 + 不同高位 → 满
    assign full  = (wr_ptr[ADDR_BITS] != rd_ptr[ADDR_BITS]) &&
                   (wr_ptr[ADDR_BITS-1:0] == rd_ptr[ADDR_BITS-1:0]);
    assign empty = (wr_ptr == rd_ptr);
    assign count = wr_ptr - rd_ptr;  // 自动处理环绕

    // ── 写操作 ──
    always @(posedge clk or negedge rst_n) begin
        if (!rst_n) begin
            wr_ptr <= 0;
        end else if (push && !full) begin
            mem[wr_ptr[ADDR_BITS-1:0]] <= wdata;
            wr_ptr <= wr_ptr + 1;
        end
    end

    // ── 读操作 ──
    always @(posedge clk or negedge rst_n) begin
        if (!rst_n) begin
            rd_ptr <= 0;
            rdata  <= 0;
        end else if (pop && !empty) begin
            rdata  <= mem[rd_ptr[ADDR_BITS-1:0]];
            rd_ptr <= rd_ptr + 1;
        end
    end

    // ════════════════════════════════════════════════════
    //               形式验证属性
    // ════════════════════════════════════════════════════
`ifdef FORMAL

    // 跟踪验证是否"热身"（至少过了一个时钟）
    reg f_past_valid;
    initial f_past_valid = 1'b0;
    always @(posedge clk) f_past_valid <= 1'b1;

    // ── Assumption：约束复位行为 ──
    // 初始状态：假设复位有效
    initial assume(!rst_n);

    // ── Assertion 1：count 永远 ≤ DEPTH ──
    // 这就是"永远不会 overflow"的形式表达
    always @(posedge clk) begin
        assert(count <= DEPTH);
    end

    // ── Assertion 2：full 时 count 必须等于 DEPTH ──
    always @(posedge clk) begin
        if (full)
            assert(count == DEPTH);
    end

    // ── Assertion 3：empty 时 count 必须等于 0 ──
    always @(posedge clk) begin
        if (empty)
            assert(count == 0);
    end

    // ── Assertion 4：push 写入的数据，下次 pop 能读出 ──
    // （如果 FIFO 是空的，push 后立刻 pop）
    always @(posedge clk) begin
        if (f_past_valid) begin
            if ($past(push) && !$past(full) && $past(empty)) begin
                // 上周期 push 了一个数据（且 FIFO 当时是空的）
                // 这周期如果 pop，应该读出那个数据
                if (pop && !empty)
                    assert(rdata == $past(wdata));
            end
        end
    end

    // ── Assertion 5：指针合法范围 ──
    always @(posedge clk) begin
        assert(wr_ptr - rd_ptr <= DEPTH);
    end

    // ── Cover：验证 FIFO 确实可以被填满 ──
    // 如果工具找不到这条路径，说明 full 信号可能永远不会触发（bug！）
    always @(posedge clk) begin
        cover(full);
        cover(empty && f_past_valid && $past(!empty));  // FIFO 从非空变为空
    end

`endif

endmodule

4.2 SymbiYosys 配置文件 .sby

# fifo_proof.sby
# SymbiYosys 配置文件

[options]
# 模式选择：
#   bmc    = Bounded Model Checking（有界模型检查）
#   prove  = BMC + Induction（无界证明）
#   cover  = 可达性检查（验证 cover 属性）
mode prove

# 深度：BMC 搜索多少步
# 对于 DEPTH=8 的 FIFO，至少需要 10 步才能填满
depth 20

# 并行化（如果 CPU 核够多）
# jobs 4

[engines]
# 使用 Bitwuzla（比 Z3 快约 2-5 倍用于这类问题）
smtbmc bitwuzla

# 备用：
# smtbmc z3
# smtbmc boolector

[script]
# 综合脚本（Yosys）
# -sv: 启用 SystemVerilog 支持
# -formal: 启用 assert/assume/cover 处理
read -formal sync_fifo.sv
prep -top sync_fifo

[files]
# 包含的源文件
sync_fifo.sv

4.3 运行证明

# 运行形式验证
sby -f fifo_proof.sby

# 输出（成功时）：
# SBY 10:23:01 [fifo_proof] engine_0: smtbmc bitwuzla
# SBY 10:23:01 [fifo_proof] engine_0: ### Checking assumptions...
# SBY 10:23:02 [fifo_proof] engine_0: ### BMC step 0...
# SBY 10:23:02 [fifo_proof] engine_0: ### BMC step 1...
# ...
# SBY 10:23:04 [fifo_proof] engine_0: ### BMC step 20... ok
# SBY 10:23:04 [fifo_proof] engine_0: ### Induction step...
# SBY 10:23:06 [fifo_proof] engine_0: ### Induction: PASSED
# SBY 10:23:06 [fifo_proof] DONE (PASS, rc=0)
#
# 总用时：约 5 秒

# 验证 cover 属性
cat > fifo_cover.sby << 'EOF'
[options]
mode cover
depth 20

[engines]
smtbmc bitwuzla

[script]
read -formal sync_fifo.sv
prep -top sync_fifo

[files]
sync_fifo.sv
EOF

sby -f fifo_cover.sby
# 输出：
# SBY [fifo_cover] engine_0: ### Checking cover...
# SBY [fifo_cover] engine_0: Cover trace for cover$line38$sync_fifo.sv:38: ok (7 steps)
# → FIFO 在 7 步内可以被填满（PASS）

5. BMC vs Induction

5.1 Bounded Model Checking（有界模型检查）

BMC 的逻辑：
"对于所有可能的初始状态 S0，
 经过 0, 1, 2, ..., k 步转换，
 属性 P 是否始终成立？"

如果 k 步内找到了反例 → FAIL（找到 bug）
如果 k 步内没有找到   → UNKNOWN（只能说：k 步内没有 bug）

BMC 是不完备的（incomplete）：找到 bug 很有效，但无法证明属性永远成立。

     初始状态
        ↓
 ┌─ Step 0 ─┐
 │ assert P │→ 成立
 └──────────┘
        ↓
 ┌─ Step 1 ─┐
 │ assert P │→ 成立
 └──────────┘
        ↓
     ...（k 步）
        ↓
 k 步内全部成立 → "可能正确"（但 k+1 步呢？）

5.2 Induction（归纳证明）

Induction 的逻辑（数学归纳法）：
1. Base Case：初始状态下，属性 P 成立
2. Inductive Step：如果在任意状态 S 下 P 成立，
   那么执行一步后的状态 S' 下，P 也成立

如果两步都通过 → P 永远成立（PROOF）

Induction 是完备的（complete），可以给出绝对保证。

但 Induction 有一个问题：归纳基可能太弱。解决方案：用 k-Induction（扩展 Base Case 到 k 步）。

5.3 SymbiYosys prove 模式

mode prove = BMC + k-Induction 组合：

# sby 的 prove 模式内部流程：
# 1. 运行 BMC（step 0, 1, 2, ..., depth）寻找 counterexample
# 2. 如果 BMC 通过，运行 Induction 尝试证明
# 3. 如果 Induction 也通过 → PROOF
# 4. 如果 Induction 失败（归纳基不够强），尝试 k-Induction

# 实际输出：
# ### BMC step 20... ok
# ### Induction: base case... ok  
# ### Induction: step case... ok
# ### DONE (PASS)

模式	命令	适用场景
`bmc`	`mode bmc`	快速寻找 bug（不能证明正确）
`prove`	`mode prove`	完整证明（需要更多时间）
`cover`	`mode cover`	验证某状态可达（测试覆盖率）
`live`	`mode live`	验证活性属性（“某事最终会发生”）

6. 反例解读：当验证失败时

6.1 故意引入 Bug

让我们在 FIFO 里引入一个微妙的 bug：

// buggy_fifo.sv
// Bug：当同时 push 和 pop，且 FIFO 即将满时，count 计算错误

// 原始（正确）：
assign count = wr_ptr - rd_ptr;

// Bug 版本：用了错误的比较（可能在 wrap-around 时出错）
assign full  = (wr_ptr[ADDR_BITS-1:0] == rd_ptr[ADDR_BITS-1:0]) &&
               (wr_ptr != rd_ptr);  // Bug：忘了处理高位！

6.2 SymbiYosys 找到 Bug

sby -f fifo_proof.sby

# 输出：
# SBY [fifo_proof] engine_0: ### BMC step 0...
# SBY [fifo_proof] engine_0: ### BMC step 1...
# ...
# SBY [fifo_proof] engine_0: ### BMC step 9... FAILED
# SBY [fifo_proof] engine_0: ### Generating counterexample trace
# SBY [fifo_proof] DONE (FAIL, rc=2)
#
# 生成反例文件：fifo_proof/engine_0/trace.vcd

6.3 查看反例 VCD

# 用 gtkwave 打开反例波形
gtkwave fifo_proof/engine_0/trace.vcd

# 或者用命令行查看（如果没有 GUI）
# 安装 vcd_parser
pip3 install vcd

python3 - << 'EOF'
import vcd

with open("fifo_proof/engine_0/trace.vcd") as f:
    tokens = vcd.tokenize(f)
    # 打印所有变量变化
    for token in tokens:
        if hasattr(token, 'value'):
            print(token)
EOF

典型的反例输出：

Time 0: rst_n=0, push=0, pop=0, wr_ptr=0, rd_ptr=0, full=0, count=0
Time 1: rst_n=1, push=1, pop=0, wdata=0xAA
Time 2: push=1, wdata=0xBB
...
Time 8: push=1, wdata=0xFF, count=8, full=0  ← Bug！count=8 但 full 没触发
Time 9: push=1  → count=9 > DEPTH=8         ← overflow！assert 失败

这就是 SymbiYosys 用 9 步找到的最短反例路径。

🚧 避坑 1：Unbounded Proof 需要 Induction，不能只用 BMC

一个常见误区：BMC 跑了 100 步没有发现 bug，就认为设计正确了。

错！BMC 只能说”前 100 步是安全的”。如果 bug 需要 101 步才能触发，BMC 发现不了。

必须用 mode prove（包含 Induction）才能给出无界证明。

判断标准：

输出 “Induction: PASSED” → 完整证明，无界安全

输出 “BMC: ok” 但没有 “Induction” → 只是有界检查

如果 Induction 一直失败（k-Induction 无法收敛），通常意味着：

你的 assume 约束不够强（初始状态空间太大）

属性本身需要辅助不变量（invariant）来辅助证明

7. 与仿真的对比：完整数字

对比维度	cocotb + iverilog 随机仿真	SymbiYosys 形式验证
发现 FIFO overflow bug	~100h（需要特定序列，概率极低）	2-5 秒
证明 FIFO 永不 overflow	不可能（只能做到概率上的信心）	5-60 秒（Induction）
学习门槛	低（Python 写测试台）	中（需要学属性语法）
代码量	测试台：100-300 行	属性：20-50 行
发现时序相关 bug	慢（需要大量状态遍历）	快（BMC 精确搜索）
发现复杂控制逻辑 bug	慢	快
发现数据路径 bug	快（直接对比输出）	需要精心设计属性
CI 集成	容易（确定性输出）	容易（sby 返回码）
最长可处理设计规模	无限制（但 bug 覆盖不保证）	~100K 门（超过会 timeout）

7.1 CI 集成示例

# .github/workflows/formal.yml
name: Formal Verification

on: [push, pull_request]

jobs:
  formal:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      
      - name: Install OSS CAD Suite
        run: |
          wget -q https://github.com/YosysHQ/oss-cad-suite-build/releases/download/2024-01-14/oss-cad-suite-linux-x64-20240114.tgz
          tar xzf oss-cad-suite-linux-x64-20240114.tgz
          echo "$PWD/oss-cad-suite/bin" >> $GITHUB_PATH
      
      - name: Run Formal Verification
        run: |
          source oss-cad-suite/environment
          sby -f fifo_proof.sby
          sby -f fifo_cover.sby
        
      - name: Upload counterexample if failed
        if: failure()
        uses: actions/upload-artifact@v4
        with:
          name: counterexample
          path: fifo_proof/engine_0/trace.vcd

🚧 避坑 2：初始状态约束

形式验证从任意可能的初始状态开始搜索，除非你用 assume 约束初始状态。

对于有复位的设计，必须告诉工具”复位后才开始验证”：
`ifdef FORMAL
// 方法1：initial assume 约束初始状态
initial assume(!rst_n);  // 从复位状态开始

// 方法2：用 f_past_valid 跳过初始状态
reg f_past_valid = 1'b0;
always @(posedge clk) f_past_valid <= 1'b1;

always @(posedge clk) begin
    if (f_past_valid) begin  // 只在第1步之后验证
        assert(count <= DEPTH);
    end
end
`endif
不约束初始状态会导致大量假反例（false counterexample）：工具从一个不合法的状态开始，找到一个”违例”——但这个初始状态在真实硬件中永远不会出现。

8. 本篇 checklist / 验证步骤

安装 SymbiYosys：sby --version 输出版本号
安装 Bitwuzla：bitwuzla --version 正常运行
对正确的 sync_fifo.sv 运行 sby -f fifo_proof.sby，看到 “PASS”
对正确的 FIFO 运行 cover 验证，看到 “full” 在 8 步内可达
故意引入 full 判断 bug，重新运行，看到 “FAIL” 和 counterexample
用 gtkwave 打开 trace.vcd，找到触发 overflow 的那一步
修复 bug，重新运行，确认回到 “PASS”
（进阶）把 sby 加入 Makefile，让 make formal 自动运行证明

🚧 避坑 3：证明时间爆炸的处理

某些设计的形式验证会卡住（SMT 求解器超时），原因通常是：
状态空间太大：设计有大量内存或宽数据总线

解决：减小参数（DEPTH=4 代替 DEPTH=256），先证明小版本
归纳基需要辅助不变量：Induction 无法收敛

解决：添加 assert 作为辅助不变量（helper invariant）
// 辅助不变量：指针差值不超过 DEPTH
always @(posedge clk)
    assert(wr_ptr - rd_ptr <= DEPTH);  // 帮助 Induction 收敛
属性写得太弱：cover 目标太难到达

解决：分解目标，先 cover 中间状态
经验法则：如果 sby 超过 5 分钟还没结束，换个更小的测试用例或简化属性。

9. 下一篇预告

开源 FPGA 04：LiteX SoC 深潜 将把工具链推向完整 SoC：

VexRiscv CPU + DDR3 + Ethernet 的完整 Python SoC 定义
litex_sim 软件仿真运行 RISC-V Linux
ECP5 真实综合：~8000 LUT，Fmax 75 MHz
LiteDRAM 带宽测试：理论 1.6 GB/s，实测 ~600 MB/s
与 Zynq PS 硬核 DDR 的代价对比

如果你已经对 FIFO 做了形式验证，把它集成进 SoC UART 缓冲区时，你可以带着”这个 FIFO 已经被数学证明是正确的”的信心——这就是形式验证的价值。

参考资料

资源	链接 / 文档号	说明
SymbiYosys 文档	symbiyosys.readthedocs.io	完整用户手册，含示例
Bitwuzla	bitwuzla.github.io	SMT 求解器，支持 QF_BV
ZipCPU 形式验证教程	zipcpu.com/formal	Dan Gisselquist 的系列教程（强烈推荐）
SVA（SystemVerilog Assertions）	IEEE Std 1800-2017 第 16 章	assert/assume/cover 完整语法
《形式化硬件验证》	Sanjit Seshia, Formal Methods for Hardware Verification	学术参考
sby FIFO 示例	YosysHQ/sby/examples/fifo	官方 FIFO 验证示例
Z3 求解器	microsoft/z3	微软研究院，备用 SMT 求解器

🦞 Kaiyo 的硬件工程日志

第一次看到 SymbiYosys 用 3 秒找到一个我的 FIFO 里藏了两周的 bug，我当场愣住了。那个 bug 需要一个非常特定的 push/pop 交替序列才能触发，随机测试跑了几天都没有发现它——但 SMT 求解器毫不费力地构造出了那条 9 步的反例序列。这就是数学的力量。