做数字IC验证这几年有很长一段时间对“验证意图”这四个字没啥感觉觉得意图就是需求文档里那几句话写进testbench就完了。直到有一次掉进一个偶发FIFO丢数据的坑随机激励跑了几个夜晚种子换了一轮又一轮覆盖率工具报出花一样的数字但那个丢数据现场就是复现不出来。后来把问题交给一位做形式验证的同事人家拿到RTL把输入端口全部声明成符号变量加了一条很短的断言半天时间就把带反例的波形trace甩到我脸上。从那天起我开始认真消化这件事传统仿真世界里的testbench SVA本质是把验证意图逼进了“有限的具体输入序列”里而把输入当成符号变量去求解能让同样的意图直接作用于整个输入空间。这就是越来越多验证团队讨论的“符号testbenchSymbolic Testbench”。本文就围绕这个概念聊聊它和SVA的关系以及怎么在实际项目里落地。1. 验证意图表达能力的两个瓶颈1.1 传统testbench只能应答“被问到的某一个输入”我们平时写的SystemVerilog testbench搭建一个UVM环境配置好virtual interface和sequence最终跑的每一个测试实际上都是对某一个具体输入场景的检查。约束随机让输入有变化但它并不会自动让输入覆盖“所有可能出现的行为”。举例来说要验证一个16深FIFO在写满后不准丢数据传统的随机BFM可能很轻易就把写侧打满但如果你同时还要保证“读写并发计数为15”这种边缘状态出现纯随机要踩到它往往靠运气。你可以在scoreboard里做出核对逻辑可以把full/almost_full保护做全但一次回归小结里能证明的始终只是“这一批向量下没出错”。这在工程上有个麻烦验证结果会被激励的概率分布“绑架”。覆盖率报告显示的90%行覆盖率不等于90%的功能意图被证实真正决定模块安全性的边界意图往往是那些随机序列短时间不容易自然触达的角落。传统testbench不是不能表达意图而是表达出来的意图永远要依附于“某一个具体观测窗口”这是它表达能力的第一个瓶颈。1.2 SVA有时序表达优势却仍然依赖事件发生SVASystemVerilog Assertions从一开始就是为了把需求翻译成可检查的时序属性存在的。它擅长表达“请求后最多N拍应答”“读使能和写使能不允许同时拉起”这一类带时钟的事件关系。在一段设计代码里加几条assert property仿真跑到对应场景后就可以快速把违规抓出来这比纯靠波形裸看出来可靠得多。但SVA在验证意图的表达上有一个容易被忽略的硬约束它是运行在仿真事件流之上的必须存在一个能驱动到对应前置条件的激励序列。如果激励从未把某个前置条件变成真那么这个断言的“通过”就只是“没机会失败”而不是“逻辑上成立”。实际工作中我们经常看到一种情况换个随机种子后原本覆盖率80%的断言突然失效原因不是代码改了而是前一版种子刚好反复踩中那个状态新种子把状态触达概率分摊淡了。SVA确实比传统testbench表达能力强了一截但它仍然默认有一个“谁来拉起场景”的外部问题这是第二个瓶颈。1.3 符号testbench要改变的是“枚举输入”这个底层方式符号testbench的思路很简单就是把输入从“在某个时刻的一个常量”上升为“一个符号变量”。测试环境不再真的给FIFO写一个字节而是告诉求解器“这一拍从din端口进来的数据可以是任何8比特组合”然后让SMT/SAT求解器去判断在所有这些可能输入组合下我声明的属性是否都能成立。如果成立等于一次性枚举了无穷多个输入场景如果不成立求解器会返回一条具体反例波形告诉你哪个输入序列可以破坏属性。这样验证意图就不再依赖某个特定测试序列来“激活”。在符号testbench的世界里验证者关心的是谓词和约束输入变量范围、状态空间可达性、安全属性与活性属性而不是具体数据流怎么走。它的代价是计算复杂度比普通仿真高很多但换来的是“验证意图覆盖范围”的质变。特别是对跨周期协议、FIFO指针、总线仲裁这一类逻辑符号testbench能给出传统方法给不出的确定性结论。2. 符号testbench与SVA各自解决的问题2.1 SVA最擅长的地方仍然不可替代业内很多人觉得SVA和符号验证是对立面实际上并不是。SVA在描述“离散事件序列是否符合预期”时的表达效率非常高比如“当valid拉起时ready必须在3拍之内拉高”这种属性放在符号检验环境里你往往也会不自觉地写成一条几乎一样的SVA目标。在IP交付、项目验收这类场合SVA也是流程里的标准配置。SVA适合的场景可以归纳为三类。第一类协议握手类request/ack/grant之间的时序关系一拍延迟两拍延迟边界非常清晰第二类状态机转换类非法状态不允许进入状态迁移条件互斥状态在指定周期内回到合法集合第三类内部数据路径的一致性检查总线数据在不同流水级之间的保持和转发关系。这些需求本质上是“对某个已发生的具体信号序列做断言”仿真能跑起来覆盖率也能做关联加上形式化验证工具可以直接消费SVA所以SVA在流程中的地位依然稳定。2.2 符号testbench覆盖的是“可能输入全集”符号testbench把验证意图拿出来的方式和SVA完全不同。它一般不会去关心某一条具体数据是不是在第三个周期被正确转发它关心的是“无论输入从哪个组合来设计状态机是否会进入非法状态”“无论占用请求怎么样总线仲裁器是否都不会同时把grant给两个人”。这里的输入是符号变量BMC求解会沿着时钟展开有限步把每一步上每个变量的所有可能取值都纳入约束。我和同行交流时发现很多人第一次接触符号testbench时会陷入一个误区认为它就是“对SVA做穷举仿真”。不对它比穷举仿真更强的点在“证明”二字。对传统仿真而言即便你跑了一百万个随机事务也没有任何逻辑能推出“第一百万零一个事务不会错”而在一个有界模型检查支持的符号环境下如果证明通过那就说明在预设深度内的所有输入序列都不违约这个结论是决定性的。如果你想把它做成无界证明再叠加k步归纳即可。2.3 选型一条务实判断标准那么到底什么时候该用SVA什么时候该上符号testbench我的经验是一句很直白的话如果模块的验证意图主要建立在“它是否按某条时钟协议动作”用SVA就足够如果模块的验证意图建立在“它在所有合法输入空间内是否都保持某种安全性质”优先考虑符号testbench。举几个实际判断的例子。一个APB从机接口的读时序在PENABLE、PSEL、PREADY那些总线协议边界组合里用SVA写property非常合适因为故障往往需要精确事件序列来暴露。但一个异步FIFO的读写指针冲突或者一组可配置寄存器在配置状态切换时的保护逻辑这种逻辑的失败通常出现在大量输入组合交汇处靠序列去找容易顾此失彼符号testbench更扎实。两种手段在真实项目里经常组合使用符号testbench做全局安全属性SVA做局部精确协议约束。维度SVA符号testbench激励来源动态仿真中的具体信号序列求解器给出的符号变量代入结论性质在已运行场景内无违例在设定深度/全局约束内无违例或返回反例依赖条件场景可触达约束可解状态可展开表达重点时序、事件、协议安全属性、可达性、不变量主要风险覆盖不到边界状态求解时间爆炸、约束过强3. 用开源工具落地第一个符号testbench3.1 准备工作与工具链说到落地这里我以开源工具SymbiYosys为例它是Yosys生态中做形式验证的入口底层引擎可以挂Boolector、Z3、Yices等SMT求解器。要注意SymbiYosys本身不是一个把testbench变成随机仿真器的工具它是以formal模式读取RTL配合.sby工程描述文件做BMC或prove。所以在你开始之前先把Yosys和SymbiYosys装好并确认能调用boolector求解器。对于商业项目Cadence JasperGold、Synopsys VC Formal也都能做同类事情理念相似你把模块顶层当作symbolic边界求解器自动实例化输入的符号变量。这里我只讲开源路径因为我自己的小规模验证实验基本都是用它完成的免费、可复现、参数透明。3.2 最小符号testbench一个FIFO指针保护例子我们用一个很常见的例子说明符号testbench的编码方式。假设有一个同步FIFO深度16写指针和读指针都是4bit计数信号cnt是5bit我们希望证明“当写使能有效且FIFO不满时写指针必须在一个周期后加1”。在传统testbench里这看起来甚至不太像断言因为它太明显了。但在符号testbench里我们需要把它写成一条属性并且让输入端口进入符号化// sync_fifo.sv module sync_fifo ( input clk, input rst_n, input wr_en, input rd_en, input [7:0] din, output logic [7:0] dout ); logic [3:0] wr_ptr; logic [3:0] rd_ptr; logic [4:0] cnt; logic [7:0] mem [0:15]; logic full, empty; assign full (cnt 5d16); assign empty (cnt 5d0); always_ff (posedge clk or negedge rst_n) begin if (!rst_n) begin wr_ptr 4d0; rd_ptr 4d0; cnt 5d0; end else begin case ({wr_en ~full, rd_en ~empty}) 2b10: cnt cnt 1; 2b01: cnt cnt - 1; default: cnt cnt; endcase if (wr_en !full) begin mem[wr_ptr] din; wr_ptr wr_ptr 1; end if (rd_en !empty) begin dout mem[rd_ptr]; rd_ptr rd_ptr 1; end end end endmodule我们关心的属性是只要写侧条件满足wr_ptr就应该在下一拍推进。不过这里有一个细节如果同周期rd_en也有效且empty为假读指针也会动但wr_ptr的推进与rd_ptr无关。为了表达这个意图可以写成property wr_ptr_advance; (posedge clk) disable iff (!rst_n) (wr_en !full) | (wr_ptr $past(wr_ptr) 1); endproperty assert property (wr_ptr_advance);注意我们在模块内部就直接写了SVA属性。这看起来似乎还是SVA对吧关键区别在于当SymbiYosys把它作为符号testbench来处理时wr_en、rd_en、din都是开放的自由输入意味着工具会尝试证明“所有wr_en、rd_en、din组合下”这条属性都成立而不是等某个testbench去随机驱动它。SVA在这里只是属性的语法载体真正的验证行为已经跑到了符号求解空间里。3.3 用SymbiYosys跑通并解读结果为了让工具按符号testbench模式执行我们创建一个.sby文件[tasks] bmc [options] mode bmc depth 20 [engines] smtbmc boolector [script] read_verilog -formal sync_fifo.sv prep -top sync_fifo [files] sync_fifo.sv然后在命令行执行sby -f sync_fifo.sby如果属性成立工具会在日志里打印类似Status: passed的结果并正常退出。如果不成立它会给出失败状态并生成带反例波形的vcd文件你可以打开波形直接看到到底是哪一组输入组合触发了矛盾。这套流程比我想象中简单第一次跑通时我最大的震撼是没有写任何driver、sequence、scoreboard只丢了一个模块和最核心的意图描述工具就自己把证明做完了。做深一点可以给task加prove和cover[tasks] bmc prove cover [options] mode bmc depth 30加上之后可以对同一个属性同时做有界检查和覆盖检查。工程实践中我通常先跑BMC验证低深度反例再切到prove模式做k步归纳看看无界空间里是否能维持结论。k步归纳要求设计具备归纳能力不是所有设计都一帆风顺但FIFO指针、计数器、简单状态机这类结构通常都适用。4. 写符号testbench的几个关键技巧4.1 有界深度和证明深度要分清跑BMC的时候depth这个参数直接决定工具往后推多少拍。很多人第一次拿到Status: passed就以为设计没问题这是个非常危险的误解。BMC通过只能说明“在展开到depth拍这个范围内没找到反例”并不代表更深一拍也成立。曾经有个同事用BMC验证一条总线授权属性depth设成8跑了半天全绿后来把depth改到16立刻抓到一个需要11拍才能暴露的冲突。所以我的习惯是先用小depth快速找反例再用大depth或切换到prove模式做接近无界的证明。prove模式下SymbiYosys会尝试用k步归纳来证明属性在所有深度上成立虽然不一定每次都成功但一旦成功结论就有真正的证明意义而不是统计意义上的“大概率没问题”。记录结论时也要在验证报告里写清楚depth和引擎不要把BMC结果当成全量证明去上报。4.2 约束写得“够窄但不够死”符号testbench里的输入虽然是自由的但不意味着所有端口都应该完全自由。如果你把一个本来只能在0到7之间取值的mode端口直接声明成3bit符号变量那么求解器会花大量时间去枚举8到15这些本不该出现的取值白白消耗计算资源还很可能给出一个“业务上不合法”的反例让debug变得混乱。正确做法是给符号变量加约束用assume property把输入限制到合法域里。比如assume property (mode 3d4);这在形式验证里等于告诉求解器“你只需要证明合法输入域内的行为”。注意约束不能太死否则会把真实缺陷也约束掉了。比如你想证明“写使能有效且FIFO不满时写指针推进”就不能额外假设wr_en只能在某些拍出现否则证明的就不是全部写场景而是你脑补的写场景。约束要表达的是环境协议而不是设计结果。4.3 先剪枝状态再上求解器符号testbench的性能瓶颈往往不是逻辑门的数量而是状态空间的展开复杂度。状态变量越多求解器需要探索的组合就越多。如果设计里有大位宽计数器、大数组或复杂数据通路直接扔给求解器等到的很可能不是结果而是内存暴涨。我常用的办法是先做抽象剪枝。第一步把与验证目标无关的数据通路去掉比如要验证FIFO的读写指针交互就不需要关心mem里存的具体字节内容可以让din保持符号但mem写使能直接指向目标位置甚至可以把mem建模成一个受约束的变量。第二步给状态变量设定合理的初值范围不要让求解器从任意瞬间的可达状态开始而是先跑一小段复位序列把状态空间压缩到真正会出现的集合里。第三步对大位宽的计数器做截断或抽象必要时用cut_point帮助求解器降低展开难度。这些操作看似在“简化设计”实际上是在把验证意图从冗余实现细节里剥出来。5. 常见问题与排错记录5.1 属性明明“想着没问题”反例却反复出现这种事最打击信心。明明代码就是常规写法属性也是照着需求文档抄的工具却告诉你有一个反例。先不要怀疑求解器绝大多数情况是属性的前置条件没写全。最典型的是漏掉disable iff条件复位期间信号抖动会直接触发违例其次是没有约束初始状态工具从默认初始化状态甚至全X状态开始展开自然可以构造出设计复位后根本不可能出现的反例。面对反例要养成先看波形的习惯。SymbiYosys会生成.vcd文件用GTKWave打开重点看反例起点和数据通路上的关键信号是不是处在真实可达状态里。如果反例里出现了“复位后第0拍wr_en就是1”这种业务上不可能的场景那说明约束少了如果反例里的输入组合在真实系统里确实会出现那恭喜你这是一个真bug抓紧提bug单去修设计。5.2 求解器跑半天不出结果是状态爆炸还是约束过松符号testbench的噩梦就是求解器跑了一夜也没有结果。这时候先别急着换更强的服务器先看日志和统计信息。如果求解器在展开到一定深度后开始反复尝试但没有新进展通常是状态空间太大导致路径枚举复杂度过高。如果深度很浅但每个cycle花的时间都极长多半是约束过松求解器在消耗大量时间处理非法输入。我个人的建议顺序是把depth降一半重跑看时间是不是线性下降。如果是指数级下降说明状态空间随深度膨胀得很厉害优先做抽象和剪枝如果降深度后时间改善不明显把注意力放到约束上检查assume属性是否把所有输入完全限制住了。工程上还有一种折中办法把一个大属性拆成多个小属性分别验证不同维度的行为减小每次求解的规模。5.3 中大规模模块的推荐切入路径如果一上来就对整个SoC子系统做符号testbench大概率会把求解器跑崩。我推荐从三个切入点开始积累经验一是深路径的控制器比如DMA、中断控制器它们状态多、随机激励很难覆盖全二是带保护逻辑的存储接口比如FIFO、AHB到APB桥指针和跨时钟交互往往藏雷三是低功耗状态切换逻辑这种模块的非法状态迁移问题非常适合用符号求解来排查。第一个符号testbench不要选太复杂的IP选一个单个模块两个时钟域以内状态变量控制在几十个bit内。先把工具链跑通把“找反例”和“读反例”的流程走顺再慢慢扩大到更大的模块。我踩过最大的一个坑就是一上来就想做整个总线的全属性证明结果数学上没问题工具在内存上先崩了白白浪费了两周。写符号testbench这件事跟我最开始想象的“高端形式验证专家专用”完全不一样。它真正提供的不是更花哨的语法而是把验证意图从“具体输入序列”中解放出来的一种思维方式。SVA依然是表达时序事件的好工具符号testbench则补上了“全输入空间下行为是否正确”这块空白。两者配合使用验证工程师才能拿回对设计质量的确定性判断力。我的体会是不用等整个团队都换工具链先挑一个模块、写一条关键属性、跑一次BMC只要体验过一次“所有输入场景都被证明无违例”的感觉就很难再回到纯靠随机激励碰运气的日子了。