前阵子帮组里同事评审一个数据通路模块的验证计划他非常认真地写了几十条SVA把握手、反压、超时、复位这些边角覆盖得挺全。我问了一句那这个模块每拍的运算结果对不对你打算怎么验证他当场愣住说回头补。我很确定他回去补出来的那几条属性多半也是用$past和局部变量硬拼出来的写的时候自己头疼维护的人更是想骂人。这个场景我相信很多验证工程师都遇到过。SVA天生是表达时序事件的说某个事件发生后几个周期另一个事件应该发生它是真强但要说每一拍ACC应该等于过去所有输入的乘积之和这种数据关系它就非常别扭。这时候真正好用的是另一种表达验证意图的方式——符号testbenchSymbolic Testbench。这篇文章不是教材算是我这几年在数据通路验证上从硬写SVA到改用符号testbench的一份实践总结。我会先讲清楚为什么SVA在数据密集型的模块上会词不达意再用一个MAC单元的完整例子把符号testbench的原理和写法讲透最后聊收敛调试和工具选择。适合正在验证DSP、编解码器、加解密单元、算术流水线或者被复杂SVA折磨过的工程师参考。1. 为什么SVA描述数据关系会越写越别扭一次关于验证意图的重新审视1.1 SVA真正擅长的是什么先说清楚我不是否定SVA。恰恰相反在我接触过的项目里SVA依然是协议验证的绝对主力。比如AHB总线的HREADY握手、AXI的通道间依赖、中断控制器的时序响应、FIFO的满空与溢出检查这些场景用SVA来表达一句话就能说清楚// 请求发出后3拍内必须收到响应 property p_req_ack; (posedge clk) disable iff (!rst_n) req |- ##[1:3] ack; endproperty这种事件在正确的时间窗口内发生的描述方式是SVA的舒适区。因为断言本身就是沿着时间轴去观察信号事件sequence、repetition、overlap这些语法元素都是为时序关系设计的。这也是为什么协议验证工程师几乎人人离不开SVA。1.2 当验证意图变成数据的函数关系但有一种场景SVA写起来会让人非常难受——累加器、乘加器、编解码器、滤波器这类模块。它们的验证意图不是某个信号在某个时刻拉高而是某个信号的数值在每一拍都应该等于某些输入数据的某种函数关系。举个最简单的例子。一个带清零端的乘累加单元期望行为是复位后ACC为0清零时ACC等于当前输入的a*b不清零时ACC等于上一拍ACC加上当前输入的a*b。如果用SVA来表达ACC每拍都等于参考模型你得这么干logic [31:0] ref_acc; always_ff (posedge clk or negedge rst_n) begin if (!rst_n) ref_acc 0; else if (clr) ref_acc $signed(a) * $signed(b); else ref_acc ref_acc $signed(a) * $signed(b); end // 然后用SVA把ref_acc和DUT输出对齐 property p_mac_match; (posedge clk) disable iff (!rst_n) acc ref_acc; endproperty你看为了让SVA能验证数据关系你必须在验证环境里额外维护一个参考模型ref_acc再用断言把这个参考模型和DUT输出对齐。这本身没什么问题但你会发现验证意图的核心其实不在SVA那段property里而在那个always_ff块里。SVA在这里沦为一个tie一个对齐检查器。更麻烦的是一旦设计里带上流水线延迟、饱和处理、溢出模式、浮点舍入这样的细节你想在SVA的property内部用局部变量手写参考逻辑或者用一长串$past去对齐流水线深度那几乎是在折磨自己。1.3 验证意图的两种形态波形属性与数据关系问题出在哪里出在我们把验证意图这个动作本身想窄了。我这几年的一个体会是验证意图其实有截然不同的两种形态。第一种是波形属性Waveform Attribute某个事件在正确的时间点发生信号之间的时序依赖符合预期。这是SVA的专长。第二种是数据关系Data Relation数据经过若干拍变换之后其结果满足某种数学期望。比如ACC等于历史所有a*b的累加。你可以用SVA强行表达它但SVA并不是为它设计的。符号testbench的核心思想就是把第二种验证意图当成一等公民来对待不强迫你用属性的语法描述数据关系而是让你用写参考模型的方式直接告诉工具正确的结果应该是什么然后让形式化引擎去证明DUT的输出和这个参考模型永远一致。这其实就是表达方式的切换从描述事件的时序约束切换为描述数据的函数关系。想通了这一点符号testbench就不再神秘了。2. 符号testbench的核心机理用证明替代枚举2.1 从动态testbench到符号testbench传统的动态testbench本质上是枚举式的你给DUT灌具体的输入值比如a5, b3观察输出是不是15。换一组值再观察。你跑一万个向量就只覆盖一万种情况。符号testbench完全换了一个思路。它让输入保持**符号symbolic**的状态——一个符号变量代表所有可能取值的任意值。工具不再逐一遍历每个具体取值而是在符号域里做推理直接回答是否存在一组输入赋值让DUT的行为违反期望我经常跟团队里的新人用这个类比动态验证是抽样检验每批货抽几个检查符号验证是全检工具在数学意义上把每一种可能性都算了一遍。如果工具证明了这个命题它不是一个跑了这么多向量都没挂的结论而是一个对于所有满足约束的输入性质永远成立的数学证明。2.2 三个核心组成部分符号变量、约束、性质一个符号testbench其实很好理解就三个核心部分符号变量对应DUT的输入数据。声明为符号后工具会自动穷举其值域范围内的所有可能。约束assume/constraint圈定合法输入空间。比如我只看a在正数范围内的行为“b的位宽虽然是16bit但协议保证了它永远小于2048”。性质assert与参考模型期望行为的描述。参考模型给出正确结果断言把DUT输出与参考模型对齐。这三件套的职责非常清楚符号变量定义我要验证什么约束定义我在什么条件下验证断言定义正确意味着什么。2.3 求解器在做什么从Miter构造到SAT证明你可能会好奇工具到底是怎么做到把所有输入组合都检查一遍的机制上形式验证引擎会把DUT和参考模型的输出接在一个异或门上——也就是构造一个miter电路——然后证明这个异或门的输出永远为0。如果DUT和参考模型有任何一拍结果不一致miter的输出就会变成1形式验证引擎的内部求解器SAT/SMT就会尝试寻找一组让这个输出为1的输入赋值。如果找到了工具输出一个counterexample反例一组具体的输入序列精确复现出错场景。如果找不到工具报告proven表示在给定的约束和帧深度范围内性质对所有输入成立。现代形式验证工具不管是Cadence JasperGold、Synopsys VC Formal还是Siemens Questa Formal用的核心算法是IC3/PDR、BMC这一类。说实话做验证的工程师未必需要消化这些算法的全部细节但理解求解器在找反例这个本质对后面调收敛、看反例非常有帮助。2.4 量化一下全检和抽样的差距为了让你直观感受符号testbench的威力我算一笔账。假设我们的DUT是一个带清零的8bit乘累加单元。输入a和b各8bit加起来16bit一共65536种取值组合。如果动态仿真想覆盖全部组合假设每个组合跑10拍来看累加行为$$65536 \times 10 655360 \text{拍}$$一台服务器跑几十万拍仿真通常要十几个小时甚至更久而且是建立在你真的能把65536个组合都作为testcase排列进去的前提下。但在符号testbench里这两条符号输入会由求解器一次性处理在配置得当的情况下往往几分钟内工具就能给出proven或反例的结果。这就是枚举和证明的本质差别。3. 实战一把用一个MAC单元讲透符号testbench的完整流程3.1 被测设计一个带清零的8bit乘累加模块先给出我们要验证的RTL设计非常简单但足够说明问题module mac #( parameter W_A 8, parameter W_B 8, parameter W_ACC 32 )( input logic clk, input logic rst_n, input logic clr, input logic signed [W_A-1:0] a, input logic signed [W_B-1:0] b, output logic signed [W_ACC-1:0] acc ); always_ff (posedge clk or negedge rst_n) begin if (!rst_n) acc 0; else if (clr) acc a * b; else acc acc a * b; end endmodule这个设计的行为规格是复位清零clr1时ACC加载当前拍的a*bclr0时ACC累加a*b。如果我们要验证的不是复位后ACC为零这种简单属性而是任意输入序列下ACC都严格等于每一拍a*b的累加或者清零后的重新累加这就不是一两条SVA能搞定的了。3.2 符号testbench的搭建参考模型驱动下面这个例子我用的是接近JasperGold Symbolic Testbench风格的写法主要为了让概念清晰。不同EDA工具的语法有差异这点我会在第6章专门讲。module symbolic_tb_mac; // ---- 时钟和复位 ---- logic clk; logic rst_n; logic clr; // ---- DUT输入输出 ---- logic signed [7:0] a; logic signed [7:0] b; logic signed [31:0] acc; // ---- DUT例化 ---- mac u_mac ( .clk (clk), .rst_n (rst_n), .clr (clr), .a (a), .b (b), .acc (acc) ); initial clk 0; always #5 clk ~clk; // ---- 符号变量声明示意具体语法以工具为准---- // 让a和b在每一拍都取任意符号值 symbolic logic signed [7:0] sym_a; symbolic logic signed [7:0] sym_b; assign a sym_a; assign b sym_b; // ---- 约束我们可以指定合法输入空间 ---- // 这里先不约束让a和b完全符号化即全值域覆盖 // 如果你想限制在非负范围assume sym_a 0; assume sym_b 0; // ---- 参考模型 ---- logic signed [31:0] ref_acc; always_ff (posedge clk or negedge rst_n) begin if (!rst_n) ref_acc 0; else if (clr) ref_acc sym_a * sym_b; else ref_acc ref_acc sym_a * sym_b; end // ---- 性质DUT输出与参考模型一致 ---- assert property ((posedge clk) disable iff (!rst_n) acc ref_acc); endmodule有的读者可能会说这不就是动态验证里的reference model assertion吗看起来没什么特别啊。关键在于数据通路输入a和b是符号变量。动态仿真会把这些变量按具体值来跑跑多少个向量就检查多少种情况而在符号testbench中a和b在每一拍都可以取任意值求解器要证明的是对于任何输入序列acc都等于ref_acc。这不是我测了这几组值没发现问题而是对于所有值性质成立。3.3 首次运行从counterexample到proven的调试全记录我第一次给类似设计跑符号testbench时遭遇了一个非常经典的反例。当时参考模型里没有正确处理clr信号——我的参考模型写成了一律累加else ref_acc ref_acc sym_a * sym_b; // 没有 if (clr) ref_acc sym_a * sym_b;DUT在clr1那一拍把ACC重新加载为a*b但参考模型还在继续累加。工具很快报出反例大致是Counterexample found: Cycle 0: a 0x05 (5), b 0x03 (3), clr 0, acc 15, ref_acc 15 Cycle 1: a 0x02 (2), b 0x04 (4), clr 1, acc 8, ref_acc 23 ^^^^^ bug: DUT已清零重载参考模型还在累加看到这个反例我第一反应不是改DUT而是先检查参考模型——因为在符号testbench的调试流程里反例既可能是RTL的bug也可能是参考模型没有正确表达验证意图。找到差异点在clr1的语义后我把参考模型补上clr分支重新跑工具很快给出Property [acc ref_acc] : PROVEN这个反例—修正—proven的循环恰恰是符号testbench最让我上瘾的地方它把验证意图和工具反馈拉得非常近每一轮迭代你都能清楚地看到到底是设计不符合预期还是你根本没说清什么是预期。3.4 这类证明的覆盖范围比动态仿真大在哪里这里补充一个容易被忽视的点。符号testbench的证明结果是**按帧frame**来算的。工具通常会证明从复位开始的任意深度内性质都成立而不是只证明某几个周期。也就是说上面那个MAC例子工具实际上覆盖了所有65536种a、b取值组合任意长度输入序列clr在任意拍为0或1的所有时间组合。动态仿真想达到同等级别的覆盖几乎是不可能完成的任务。这也是我在数据通路验证场景下越来越依赖符号testbench的根本原因。4. SVA与符号testbench的分工日常项目中该怎么选4.1 一张表搞清楚边界很多工程师容易陷入学了什么就什么都用它的思维定式。我见过有人用符号testbench去验证状态机跳转也有人用SVA硬验FFT蝶形运算单元结果都是痛苦不堪。下面这张表是我自己项目里的选型参考分享出来对比维度SVA符号testbench核心表达对象事件、时序、状态跳转数据变换、算术关系、流水线一致性典型场景总线协议、握手、FIFO、复位序列、状态机MAC、DSP、编解码、加解密、数据通路表达方式属性语言sequence、property参考模型 符号变量 断言证明方式形式验证或动态仿真均可主要依赖形式化引擎证明输入覆盖受限于仿真向量或形式抽象符号化穷举参考模型不常用靠属性描述预期核心组件直接定义预期调试手段波形、断言命中/失败报告counterexample波形分叉点回溯上手门槛中等语法需熟练低会写SystemVerilog就能上手4.2 选型判断流程一个简单的两问法我在评估一个模块该用哪种验证方式时一般先问自己两个问题第一步验证的核心意图是事情的顺序还是数据的数值如果是前者比如读请求发出后数据不能在写数据之前返回那毫不犹豫用SVA。如果是后者比如解码器输出的每个像素都应该等于编码器输入的像素经过量化后的结果那符号testbench是更自然的选择。第二步这个模块是控制密集型还是数据密集型一个AHB-to-APB桥是典型的控制密集型它的正确性几乎全部体现在时序握手和状态转移上而一个8bit × 8bit的MAC单元是典型的数据密集型握手逻辑可能只占5%剩下95%的验证价值都在数值算得对不对上。控制密集用SVA数据密集用符号testbench混合型就分层处理。4.3 混合使用的实践SVA管协议符号testbench管数据现实中的模块很少是纯数据或纯控制的。以我最近验证的一个图像处理IP为例AXI-S接口负责输入输出流内部是一段流水线做像素变换。我的做法是分两层在AXI-S接口层用SVA覆盖ready/valid握手、通道间依赖、last信号行为在内部像素数据通路层用符号testbench把输入像素和系数作为符号变量参考模型直接写正确的像素变换结果证明流水线输出永远等于参考模型。这两个验证环境可以并行开发。SVA那层更像交通规则检查符号testbench这层更像算账核对。两者各有各的职责互不干扰但合在一起模块的验证闭环才算真正完整。这也是我理解的表达验证意图的完整含义不同性质的意图用不同的表达方式而不是强迫某一个工具/语言去解决所有问题。5. 收敛与调试符号testbench真正考验人的地方5.1 最常见的失败形态与根因符号testbench不是银弹。说得直接一点大部分人在第一次接触时都会在收敛这件事情上栽跟头。工具跑了半天不结束或者随便就给你甩出一堆反例都很正常。根据我的经验失败形态大概有这么几类第一类是状态爆炸。符号变量太多、位宽太大、参考模型里用了太复杂的运算尤其是乘法器、除法器、非线性函数都会让形式化引擎的搜索空间爆炸式增长。我见过有人试图把一个32bit乘法器的所有输入组合全符号化结果跑了24小时还没收敛。第二类是约束设计不合理。约束太强证明结果没有意义——比如你把a约束成永远等于b工具当然很好证明但验证价值等于零约束太弱工具会找到大量无关紧要的反例或者根本不知道该往哪个方向搜索。第三类是参考模型与DUT的语义偏差。这是最隐蔽的坑。复位时序差了一拍、饱和模式没对齐、溢出截断方式不同、clr优先级定义不一致任何一点点偏差都会让工具报出一堆反例而且如果你不细看还会误以为DUT有bug。实际上很多时候是参考模型没有精确表达验证意图。5.2 调试Counterexample的完整思路拿到一个counterexample我一般按三条路线排查看分叉点。反例波形里DUT输出和参考模型一定是从某一拍开始不一致的。找到第一个不一致的拍用波形工具放大看这一拍的输入条件这往往直接指向问题源头。确认最小反例。好的工具会给出最短的复现序列。看这个最短序列中哪些输入是真正触发不一致的关键条件——是clr1还是某个特定数据值一旦定位到关键条件问题就缩小到这个条件下参考模型的行为是否正确。判断是谁的错。不要默认RTL有bug。我会先看参考模型在这一拍的行为是否符合规格书描述。如果参考模型的行为本身就不对那是验证环境的错误如果参考模型行为正确而DUT输出不对那才是RTL bug。这里有个技巧我一直用在参考模型里刻意加一些哨兵断言比如assert (ref_acc expected_value)用来验证参考模型自身是否在正确工作。如果哨兵断言能过但DUT和参考模型不一致那问题大概率在DUT侧。5.3 收敛调优的几个实战经验以下经验是我在实践中反复验证过的可以帮你少走弯路把控制信号和数据信号分开抽象。控制信号clr、en、valid通常用枚举数据信号a、b用符号化。不要一股脑全符号化控制信号的符号化很容易导致状态爆炸。大位宽数据拆段验证。一个32bit乘法器全符号化很难收敛但分成高16位和低16位分别验证或者在约束里限制输入范围往往能大幅降低求解难度。善用cutpoint切割点。如果参考模型里某个中间信号过于复杂可以把它设成cutpoint让引擎在中间值上自由发挥把问题拆成两段来证明。这相当于把一个难问题切成两个容易问题。约束要复核可满足性。工具一般会检查assume是否consistent但工程师也要主动确认约束没有把合法场景排除掉。一个简单的办法是把约束复制到动态仿真里跑一跑看随机出来的激励是否符合预期分布。建立一个经过验证的参考模型库。同一个算法家族的模块各种MAC、FIR、CRC、S盒参考模型高度相似。我建议团队把验证过的参考模型沉淀成公共库新项目直接复用不要每次从头写——参考模型写错导致的反例潮是时间黑洞。6. 工具支持的现实差异JasperGold、VC Formal、Questa Formal6.1 三大EDA工具的符号testbench能力说到实际落地就必须聊工具。目前三大主流形式验证工具都对符号testbench有不同程度的支持但语法和工程体验差异不小工具对应功能/模式特点Cadence JasperGoldSymbolic TestbenchSTB最成熟技术文档多参考模型符号变量约束是原生概念调试环境Visualize强大Synopsys VC FormalDatapath Validation / Formal TestbenchFlow走App化的路线内置一些数据通路验证场景模板适合按流程操作Siemens EDA Questa FormalFormal Testbench / Symbolic Simulation符号模拟能力不错但社区资料相对少上手时更需要熟悉自家SDG以我自己的体验JasperGold对符号testbench的支持最接近我在第3章写的那种直觉式写法声明symbolic变量、写参考模型、写assert property然后工具自动帮你做全帧证明。VC Formal的App化思路也很实用适合团队里不想深挖原理、按向导操作就能跑出结果的场景。Questa Formal的符号模拟更适合在小规模模块上做快速验证。6.2 语法迁移概念一致别被工具绑定不同工具间迁移时最大的障碍是语法细节比如符号变量声明方式、约束的写法、参考模型的组织方式。但我想强调的是核心概念完全一致符号变量 约束 参考模型 断言这四件事在任何工具里都是符号testbench的骨架。我自己的做法是参考模型用可移植的标准SystemVerilog来写尽量不依赖工具的扩展语法。这样从一个工具迁移到另一个工具时只需要改符号变量声明和约束语法这两小段参考模型本身可以原封不动地带过去。这也算是降低团队工具锁定风险的一个小技巧。6.3 团队落地从小模块试点做起最后给想引入符号testbench的团队一点落地建议。不要试图一上来就把所有数据通路模块都改成符号验证那一定会被项目节奏和团队接受度拖垮。我的建议是先找一个规模适中的计算模块比如一个8bit的MAC、一个小点数的FIR滤波器搭一个最小的符号testbench跑通proven。然后带着这个proven结果和动态仿真的覆盖率报告做对比让团队直观看到全检和抽样的差距。有了第一个成功案例后面再推广就顺理成章了。另外务必要培养团队reference model first的思维方式。符号testbench的核心资产是参考模型它不是测试代码而是验证意图的正规化描述。这个资产积累下来复用价值非常高。最后说句实在话。我现在的习惯是接到一个数据通路模块先不急着想SVA要写哪几条而是先问自己——我到底想向工具证明这个模块应该算什么数这个问题一旦想清楚用符号testbench表达出来往往只需要几十行代码比硬憋一百多条断言轻松得多。符号testbench不是什么高深的新技术但它确实提供了一种SVA之外的、更贴近数据验证意图的表达方式。如果你手上正好有个算术模块把你折磨得够呛我建议你找一个周末搭一个最小的符号testbench试试哪怕只验证一个8bit的MAC。等工具在几分钟内告诉你proven、而同事还在那里凑仿真覆盖率的时候你会回来感谢我的。