企业官网建设流程全解析

PLFM_RADAR形式化验证实战：用SymbiYosys证明跨时钟域握手正确性

【免费下载链接】PLFM_RADAROpen-source, low-cost 10.5 GHz PLFM phased array RADAR system项目地址: https://gitcode.com/GitHub_Trending/pl/PLFM_RADAR

PLFM_RADAR（AERIS-10）是一个开源、低成本的 10.5GHz 脉冲线性调频（PLFM）相控阵雷达系统。在这套雷达的 FPGA 信号处理链中，ADC、DAC、时钟合成器与处理器工作在不同时钟域，跨时钟域（CDC）数据传递的正确性直接决定雷达能否稳定工作。本文将带你实战用SymbiYosys对 PLFM_RADAR 中最关键的 CDC 握手模块进行形式化验证，证明 req/ack 握手协议在任意时钟交错下都不会出错。

为什么雷达 FPGA 必须做跨时钟域验证？

在 PLFM_RADAR 的接收链路中，400MHz ADC 采样数据需要降采样到 120MHz 基带，再做脉冲压缩、Doppler FFT、MTI 和 CFAR 处理。这些模块分别挂在不同的时钟域上，跨时钟域传输数据时，如果只是简单地把信号直接打拍同步，多比特数据可能在目标域采样到"一半新、一半旧"的混合值，造成雷达数据损坏——这就是经典的 CDC 亚稳态问题。

传统做法是依赖综合工具（如 Vivado 的report_cdc）做静态检查，但它只能发现"哪里有跨域"，无法证明"跨域协议是否正确"。PLFM_RADAR 的做法更进一步：用形式化验证（Formal Verification）穷举所有可能的时钟交错与数据序列，在数学层面证明握手协议的正确性。

认识 SymbiYosys：开源形式化验证工具链

SymbiYosys（sby）是 Yosys 生态下的开源形式化验证框架，由四个核心部件组成：

• Yosys：负责把 Verilog 解析并转换成形式化求解所需的逻辑网络
• SMTC：将属性断言转换为可满足性（SAT）问题
• smtbmc：通过 SMT 求解器（如 Z3、Boolector）进行有界模型检查（BMC）和可达性分析（cover）
• clk2fflogic：将多时钟设计转换为单时钟的"逻辑等价"模型，这是验证 CDC 模块的关键

在 PLFM_RADAR 中，所有形式化验证脚本都放在9_Firmware/9_2_FPGA/formal/目录下，覆盖了单比特同步器、ADC 接口、Doppler 处理器、雷达模式控制器等关键模块。

实战第一步：搭建多时钟形式化验证环境

先看最关键的握手验证配置 fv_cdc_handshake.sby：

[tasks] bmc cover [options] bmc: mode bmc bmc: depth 100 cover: mode cover cover: depth 200 [engines] smtbmc z3 [script] read_verilog -formal cdc_modules.v read_verilog -formal fv_cdc_handshake.v prep -top fv_cdc_handshake clk2fflogic [files] ../cdc_modules.v fv_cdc_handshake.v

要点解读：

• 双任务并行：bmc（有界模型检查）在 100 拍内搜索反例；cover（可达性分析）在 200 拍内寻找关键协议状态能否到达
• 求解器选择：smtbmc z3，Z3 对位向量逻辑求解效率高，适合 CDC 这类状态密集问题
• clk2fflogic是灵魂：它把异步时钟转换成统一的 formal clock 逻辑，让求解器可以自由地让两个时钟"随便交错"，从而穷举所有异步时序可能

实战第二步：让求解器自由生成异步时钟

在 fv_cdc_handshake.v 中，验证环境用$anyseq让求解器随意决定每个形式化周期两个时钟是否翻转：

assign src_clk_en = $anyseq; assign dst_clk_en = $anyseq;

这意味着 src 域和 dst 域可以以任意频率比、任意相位关系交错——这正是真实异步时钟最恶劣的情况。同时，环境还添加了时钟活性约束（每个时钟 7 个 gclk 周期内必须翻转一次），防止求解器"偷懒"让时钟永远静止来逃避检查。

实战第三步：7 条核心断言证明握手协议

DUT 是 cdc_modules.v 中的cdc_handshake模块：源域锁存数据、置起src_busy，经两级同步器把请求传到目标域，目标域捕获数据、回送dst_ack，再经两级同步器传回源域清除 busy。这是一个标准的 4 相位握手。

验证环境针对它写下了 7 条断言：

1. 结构性不变量：src_ready == !src_busy，确认握手信号定义一致
2. 复位行为：复位期间所有输出必须保持无效电平，内部状态清零
3. dst_valid有界时长：有效信号不能无限拉高（上限 60 拍）
4. 数据稳定性：dst_valid有效期间，dst_data必须保持不变——这是防止"数据被半路篡改"的关键证明
5. 忙信号有界活性：src_busy拉高后必须在 100 拍内恢复（前提是目标域 8 拍内响应）
6. dst_ack有界时长：应答信号必须及时清除（上限 50 拍）
7. 同步链状态有界：两级同步链寄存器必须保持在合法取值范围内

这些断言组合起来回答了三个核心问题：数据会不会丢？数据会不会错？系统会不会死锁？这正是 CDC 握手验证的全部意义。

实战第四步：用 cover 证明协议真的"走得通"

断言只能证明"坏事情不会发生"，但无法证明"好事情真的会发生"。所以验证环境还加了 4 条 cover：

• 源域成功接受数据（src_valid && src_ready）
• 目标域成功呈现数据（dst_valid）
• 目标域成功消费数据（dst_valid && dst_ready）
• 完整往返：一次传输结束后源域重新回到 ready 状态

如果某条 cover 无法到达，说明协议虽然"安全"但存在"卡死路径"——这也是形式化验证能发现的最隐蔽缺陷之一。

配套验证：单比特同步器与 ADC 接口

除了多比特握手，PLFM_RADAR 还对基础单比特同步器做了形式化验证（fv_cdc_single_bit.sby），证明两条性质：

• 复位期间输出必须为 0
• 输出只在目标时钟上升沿变化：没有目标时钟边沿时输出必须保持稳定，这是同步器的基本正确性要求

ADC 接口（fv_cdc_adc.sby）则用同样的方法验证了 400MHz ADC 数据跨域采集路径。这些验证脚本与 Vivado 的report_cdc静态检查（见 run_cdc_and_netlist.tcl）形成互补：静态检查回答"哪里有跨域"，形式化验证回答"跨域是否安全"。

运行验证与解读结果

在装有 Yosys/SymbiYosys 的环境中，运行方式非常简单：

cd 9_Firmware/9_2_FPGA/formal sby -f fv_cdc_handshake.sby

如果所有断言都通过，你会看到每个任务都报告PASS。如果某个断言被破坏，smtbmc 会输出一个反例波形（trace），告诉你具体的时钟交错和信号序列导致失败——这种级别的可诊断性是仿真测试很难提供的。

值得一提的是，PLFM_RADAR 的验证环境为降低求解难度做了精心设计，例如：

• 握手数据位宽从 32 位降到 8 位（parameter WIDTH = 8），显著加快求解
• 使用有界时长断言替代精确周期断言，规避clk2fflogic引入的流水线延迟
• 用dut_initialized门控断言，确保属性只在 DUT 完全复位后才生效

总结：形式化验证是雷达可靠性的数学保证

PLFM_RADAR 用 SymbiYosys 为跨时钟域握手写下的这套验证环境，代表了开源硬件验证的最佳实践：

1. 多时钟建模：用$anyseq+clk2fflogic穷举异步时钟交错
2. 活性与安全双管齐下：断言证明安全，cover 证明活性
3. 可诊断性：反例 trace 能精确定位失败场景
4. 开源可复现：整个验证环境就在9_Firmware/9_2_FPGA/formal/目录中，任何人都能复现

对于任何涉及多时钟域的 FPGA 设计——尤其是雷达、通信这类对可靠性要求极高的系统，这套"用数学证明替代运气"的验证思路，都值得借鉴。克隆 PLFM_RADAR 仓库后，亲手跑一遍sby -f fv_cdc_handshake.sby，你会对"形式化验证证明握手正确性"有最直观的体会。

【免费下载链接】PLFM_RADAROpen-source, low-cost 10.5 GHz PLFM phased array RADAR system项目地址: https://gitcode.com/GitHub_Trending/pl/PLFM_RADAR