做验证的朋友这几年应该没少听到“VC Formal”这个组合词。很多团队在评估验证效率时从纯动态仿真转向形式化验证发现那些边角问题、溢出问题、跨周期耦合问题一抓一个准。我在这条路上也折腾了不少回合从最开始连 property 怎么写、约束怎么下都搞不清到后来能在几天之内把一个小模块的 formal 环境完整搭起来中间踩过的坑值得系统记录下来。这篇文章就以一个同步 FIFO 的实例为主线把 VC Formal 的完整流程走一遍。如果你正在评估引入形式化验证或者团队刚拿到 license 不知道从哪里落地这篇文章应该是现阶段最需要的参考。1. 从一次仿真崩溃说起Formal 到底在解决什么1.1 动态仿真的盲区我先讲一个真实场景。某个模块的功能仿真覆盖率跑到了 98%回归用例整夜跑完一条都没挂掉。结果一到上板联调系统偶发死锁复盘下来发现是两个几乎没有互动的控制信号在某个特定时序窗口打架。这种窗口随机约束要命中的概率大概是百万分之一。你说这是设计问题还是验证问题严格讲是验证完备性的问题因为动态仿真本质上是一个“抽样”过程而 formal 是一个“穷举证明”过程。只要约束建得正确形式化验证会把模块的所有可达状态全部推一遍不会漏掉这种低频窗口。这也是我后来在验证计划里把 formal 列为必做项的原因。1.2 VC Formal 的能力边界VC Formal 是 Synopsys 的形式化验证平台总称不是某一个单独的小工具。它覆盖的能力包括断言证明property verification、时序等价性检查sequential equivalence checking、X 态传播分析、覆盖率补充以及一些针对特定设计场景的 app比如数据通路验证datapath validation。在项目里最常见的用法是把动态仿真难以覆盖的场景用断言加约束的方式放进 formal 里跑。对一个用 SVA 或 PSL 写出的属性VC Formal 会去遍历所有可达状态只要属性在任意合法输入序列下不成立它就能在有限步数内找到反例并给出波形如果属性成立引擎也会给出证明状态。你不需要手工枚举完整状态空间背后的 BDD、SAT、SMT 以及大量抽象化简技术会替你做这件事。2. 验证对象与用例设计同步 FIFO 的形式化验证目标2.1 为什么拿同步 FIFO 当切入点同步 FIFO 是几乎所有设计都会用到的模块规模不大但麻雀虽小五脏俱全——读写指针、空满标志、数据通路、溢出读空行为全都有。用 formal 验证 FIFO 的属性比写 testbench 做定向仿真干净得多。比如“满标志必须和计数器深度精确绑定”这种属性用动态仿真你得反复构造读写序列来碰而在 formal 里只需要把稳定的逻辑关系写清楚工具会自动把各种读写交错路径都跑一遍。2.2 一个可复现的同步 FIFO 实现下面这个 RTL 是我平时做演示常用的版本深度 8读延迟一拍读写指针循环使用。// sync_fifo.sv module sync_fifo #( parameter DATA_WIDTH 32, parameter DEPTH 8 )( input logic clk, input logic rst_n, input logic wr_en, input logic [DATA_WIDTH-1:0] din, input logic rd_en, output logic [DATA_WIDTH-1:0] dout, output logic full, output logic empty ); localparam ADDR_WIDTH $clog2(DEPTH); logic [DATA_WIDTH-1:0] mem [DEPTH]; logic [ADDR_WIDTH-1:0] wptr, rptr; logic [ADDR_WIDTH:0] count; always_ff (posedge clk or negedge rst_n) begin if (!rst_n) begin wptr 0; rptr 0; count 0; end else begin case ({wr_en ~full, rd_en ~empty}) 2b10: count count 1b1; 2b01: count count - 1b1; default: ; endcase if (wr_en ~full) begin mem[wptr] din; wptr wptr 1b1; end if (rd_en ~empty) begin dout mem[rptr]; rptr rptr 1b1; end end end assign full (count DEPTH); assign empty (count 0); endmodule这里有几个设计点需要留意。count 的位宽是 ADDR_WIDTH1而不是 ADDR_WIDTH因为 count 需要表示 0 到 DEPTH正好比指针多一位。full 和 empty 完全由 count 导出而不是根据指针相等判断这样空满逻辑更直观也给 formal 提供了明确的对照基准。dout 是寄存输出所以读操作发出 rdata 会晚一拍这类时序关系在写断言时必须心里有数。2.3 形式化验证的三个基本要素一个 formal 环境无论目标多复杂本质上只有三件事时钟与复位、输入约束、断言属性。时钟决定时间推进复位决定初始状态约束划出合法输入的边界断言描述必须要成立的行为。很多新人一上来就写断言漏掉环境约束结果证明出一堆 vacuous pass或者工具跑了半天给你报 inconclusive原因往往就出在这三者的设定不完整。打个比方formal 就像一座封闭建筑时钟是挂钟复位是入场安检约束是参观动线断言是建筑必须满足的承重规范。动线没约束好访客到处乱逛某些房间看似检查过其实根本没人进去。3. 环境准备与文件搭建3.1 工具与 license跑 VC Formal 的硬性门槛是 license 里要有 Formal 相关 feature。实际工程中很多公司采购的是 simulation 和 formal 的组合 license需要确认工具能拿到可用的 formal feature。启动前可以用许可管理命令查一下具体 feature 名称不同版本略有差异以 license 文件里的标注为准。另一个容易忽略的点是版本配套如果设计里用了较新的 SystemVerilog 语法比如 interface、class、随机约束等要保证工具版本能完整解析这些语法否则 read 阶段就会莫名报错。3.2 工程目录结构formal 验证最大的敌人是工程不可复现。昨天能出结果的设置今天换台机器跑不出来了大多是因为环境文件散落各处约束和属性混在一起改乱了。我习惯用下面这套目录结构fifo_formal/ ├── rtl/ │ └── sync_fifo.sv ├── tb/ │ ├── fifo_env.sva │ └── fifo_properties.sva ├── scripts/ │ ├── setup.tcl │ └── prove.tcl └── run/rtl 目录只放设计源文件tb 目录里区分环境约束文件和验证目标文件scripts 放批处理脚本run 目录放工具生成的工程文件、日志和反例波形。约束文件和断言文件必须物理分开这一点非常重要。因为开发阶段你可能要频繁调整约束如果和断言混在同一个文件里容易误改验证目标而不自知。3.3 启动方式的选择VC Formal 有图形界面也支持脚本驱动的批处理模式。我的建议是先把脚本流程跑通再用 GUI 打开同一份工程查看结果和波形这样既方便调试也能把最终环境纳入回归。脚本驱动的另一个好处是方便做版本管理整个验证环境的配置都能被 review而不是依赖个人在图形界面里点出来的状态。4. 断言与约束的完整编写4.1 FIFO 的核心断言集下面这份属性文件覆盖了 FIFO 最关键的正确性条件。为了在模块外部引用内部信号实际工程里常常用 bind 把验证环境绑到 DUT 上这里我直接用 bind 方式示意。// fifo_bind.sv bind sync_fifo fifo_properties fifo_properties_inst (.*); bind sync_fifo fifo_env fifo_env_inst (.*);属性文件内容如下// fifo_properties.sva module fifo_properties; // p1: 空标志必须与 count0 严格等价 ap_empty_eq_count0: assert property ( (posedge clk) disable iff (!rst_n) (empty (count 0)) ); // p2: 满标志必须与 countDEPTH 严格等价 ap_full_eq_count_depth: assert property ( (posedge clk) disable iff (!rst_n) (full (count DEPTH)) ); // p3: count 永远不越界 ap_count_range: assert property ( (posedge clk) disable iff (!rst_n) (count DEPTH) ); // p4: 复位后进入一致状态 ap_reset_init: assert property ( (posedge clk) ($past(!rst_n) rst_n |- empty !full count 0) ); endmodule每条断言的意图要清楚。p1 和 p2 分别锁定空满标志与 count 的等价关系确保空满逻辑没有被多余的组合逻辑干扰。p3 是值域上界检查防止 count 出现异常跳变。p4 检查复位释放后的第一个周期FIFO 是否能进入一致的空状态。注意 p4 里用到了$past(!rst_n) rst_n这需要保证在前一拍确实是复位态否则属性会变得没有意义。4.2 输入约束环境让读写行为合法化单独有断言还不够还必须对输入行为做约束。真实环境中写方和读方都应当遵循“不满时才能写不空时才能读”的协议。如果约束缺失工具会把同时写满、同时读空这些非法场景也当成合法输入导致设计被判定为有 bug但那其实是你给的输入不合法。// fifo_env.sva module fifo_env; // 约束写请求只有在非满或复位态下才允许拉高 constr_wr_not_full: assume property ( (posedge clk) (!rst_n || !full) || !wr_en ); // 约束读请求只有在非空或复位态下才允许拉高 constr_rd_not_empty: assume property ( (posedge clk) (!rst_n || !empty) || !rd_en ); // 活性辅助保证存在一种路径能让 dout 被更新 sanity_rd_path: assert property ( (posedge clk) disable iff (!rst_n) (rd_en |- !empty) ); endmodule上面这个活性辅助断言值得多说两句。它看着像一条普通断言但它的作用在于“传感器”如果约束环境把读路径屏蔽了rd_en 永远拉不高这条断言就会以 vacuous 的方式通过你会发现它从未被真正触发过。这时候就要回头检查约束是不是写得太强。给 formal 环境加一个活性探测器能有效防止假通过。4.3 约束和断言必须分清的两个概念约束assume和断言assert在 VC Formal 里的地位完全不同。约束把输入空间框起来约束被违反不算 bug工具只会忽略那条路径断言则是设计必须满足的行为断言失败就证明设计有缺陷。误把约束写成断言工具会报出无数个“设计 bug”其实是你自己给的输入不合法反过来把断言写成约束问题会被直接隐藏变成最危险的 vacuous pass。我在代码评审时首先看的就是约束文件里有没有混入本应属于验证目标的逻辑。5. 跑通 VC Formal编译、证明与结果解析5.1 脚本流程的整体骨架我通常不在 GUI 里逐个点命令而是先把批处理脚本跑通脚本结构大概是下面这样。需要说明的是具体命令名在工具不同版本里可能略有差异但流程骨架是一致的拿到实际环境后对照工具文档做微调即可。# prove.tcl # 1. 读取设计 read_verilog -sverilog ../rtl/sync_fifo.sv # 2. 设置验证对象 set_top sync_fifo # 3. 定义时钟与复位 create_clock clk -period 10 create_reset rst_n -active_low # 4. 读入约束和属性 read_sva -sv ../tb/fifo_env.sva read_sva -sv ../tb/fifo_properties.sva # 5. 发起证明 prove_property -all这里有几个参数值得解释。-period 10只是给时钟一个周期定义很多属性证明不依赖真实周期长度除非断言里使用了##[1:N]这类周期延迟。延迟窗口越大搜索深度越深计算消耗也会明显上涨。create_reset指定复位信号和有效电平工具会从复位释放后的状态开始展开时间帧因此复位建模错误会让整个证明跑偏这一步需要反复确认。5.2 时间深度与证明压力的权衡证明一个属性时工具会从初始状态逐步展开时间帧。比如ap_full_eq_count_depth要从复位状态一路写到 count 满需要经历多个读写周期引擎会自动寻找足够的展开深度。如果属性迟迟不收敛可以显式设置最大深度但不能一上来就把深度调得很大那会让证明时间指数级上升。我的做法是先用小深度快速扫描看有没有反例确认没有后再逐步加深。搜索深度和证明时间是一对矛盾需要根据模块复杂度找到平衡点。5.3 结果状态解读证明跑完后的结果通常有几种状态我看结果时有一套固定心法状态含义处理建议proven属性在约束空间内成立可以信任但注意排查 vacuousfalsified找到反例打开波形重点分析起点状态inconclusive搜索深度不足或资源受限调整边界拆分属性或加深限制vacuous属性前提从不成立检查约束是否过强补活性断言特别是 vacuous 这种情况多数工具不一定直接标注你得自己检查属性左边的条件到底能不能被触发。以前我带团队时有同事因为约束写太强把写使能完全屏蔽结果空满属性全部 proven但整个环境根本没有在测设计这种通过比证明失败更坑因为没人会怀疑它。5.4 用反例波形的起点定位问题当工具报 falsified 时先把 counterexample 波形打开。重点看反例的起点是从复位后不久就出现还是跑到很深才出现。如果是前者多半是约束写得不对导致输入的初始行为不合法如果是后者说明这是一个跨周期的深边界问题需要认真分析设计逻辑。我实际调试时大部分时间不是在改设计而是在改约束。把自己放到工具的位置上想一想它为什么认为这条路径合法如果它合法设计为何会错顺着这个思路走定位效率会高很多。6. 常见问题与排查技巧实录6.1 证明超时或者不收敛超时是 formal 的头号问题。遇到这种情况先从属性本身下手把大属性拆成小属性或者加一些辅助断言做 cut point降低单次证明的复杂度。另一个常用手段是限制输入数据位宽比如 FIFO 的数据位宽是 32 位但数据通路的属性证明可以先在 4 位或 8 位宽下做验证如果数据通路逻辑没有按位耦合结果可以外推。约束松则证明难约束紧则证明快但结果正确性也更受约束限制这个度需要根据设计特点来拿捏。6.2 假通过vacuous pass 的排查假通过几乎是每个 formal 新手都会遇到的坑。怎么排查看工具报告里每个属性的触发次数统计。如果某个属性从未被真正评价过工具仍然可能直接标 proven这时候就需要人工介入。我的习惯是在约束环境里带一个活性辅助断言保证读、写路径都能被激活。这样环境不会“死”属性也不会在空转状态下通过。另一个辅助手段是故意在 RTL 里临时插一个 bug验证工具能不能发现。如果插了 bug 但属性仍显示 proven那环境一定有问题。6.3 搜索词里的一堆“VC”和“formal”搜索“vc formal”的时候经常跳出来一堆让人迷惑的词。Visual C 的运行库、VC 环境修复、ISE 14.7 和 MSVC 2008 的兼容问题、CBuilder 的 VCL DLL、VMware 的 vCenter缩写也是 VC还有微信小程序模板消息里的 miniprogram_stateformal那个参数表示跳转正式版。这些和本文讨论的 VC Formal 完全不是一回事。有些朋友在 Windows 下折腾 VC 运行库报错或者在 VMware 环境里看到 vCenter 的告警跑到 formal 教程里来找答案自然觉得牛头不对马嘴。先把这个词义辨析清楚能省掉不少冤枉时间。6.4 运行环境依赖的小坑顺便说一个环境依赖问题。很多人以为 VC Formal 只运行在 Linux 服务器上其实部分辅助脚本或图形化组件也有 Windows 版本于是就会遇到各种 VC redistributable 弹窗。我之前在 Windows 下配置辅助工具时明明装了一堆运行时仍然提示缺库最后发现是 32 位和 64 位运行库没装全或者动态库被安全软件隔离了。在 Linux 服务器上更常见的是缺少 glibc、libXext 这类基础库。这类环境问题和 formal 本身无关但确实会消耗团队时间。我的建议是固定一套经过验证的基础环境镜像把工具依赖一次装齐不要每次在新机器上从零折腾。6.5 从 FIFO 放大到真实模块同步 FIFO 只是一个最小可运行的切入点。实际项目中我会把同样的目录结构、同样的三段式模板套到仲裁器、AXI 桥、寄存器阵列这些模块上。区别只是约束复杂度和 prove 深度。VC Formal 的价值不是把每个模块都完整证明一遍而是在动态仿真覆盖率长期卡住的区域精准补刀。比如仲裁器的公平性、AXI 桥的出栈乱序、握手协议的死锁可能性这些靠仿真很难给出确定结论formal 却能给出明确结果。最后再分享一点个人体会。第一次接触 formal 任务时不要一上来就追求把所有属性都 prove先把约束环境和对空满标志的 sanity check 证明出来。这个过程能让你学会跟工具“对话”它报 falsified你去查约束它报 timeout你去查抽象范围。等这套手感建立了再往复杂属性上走就顺了。我自己的习惯是给每个 formal 环境都保留一个专门验证环境活性的属性像传感器一样确保约束不是一堵把问题挡在外面的死墙。