1. 验证意图SVA并不是唯一答案做芯片验证这些年我一直有个感受SVASystemVerilog Assertions几乎成了“表达验证意图”的代名词。不管是协议检查、时序约束还是覆盖率收集大家都习惯性地用断言去描述“设计必须满足什么”。SVA也确实好用尤其在动态仿真里一条断言挂在接口上跑回归的时候就能实时盯着关键时序发现问题直接报错效率很高。但SVA也有它力不从心的时候。举一个很常见的例子你想验证一个计数器在任意起始值、任意使能序列下最终能否在10个周期内输出一个溢出标志。用SVA写你只能写“如果使能连续拉高10拍则溢出信号在第10拍拉高”这种带限定前缀的属性可一旦使能不是连续的、起始值不是0这类基于确定场景的断言就覆盖不了。你真正想问的问题是“有没有可能在某些输入序列下设计会进入某个特定状态”换句话说你想验证的不是“给定激励的结果”而是“激励空间里是否存在一条路径能到达某个条件”。这个问题SVA表达起来很别扭。我第一次意识到这个问题是在一次覆盖率收敛会上。团队拿着一个数据通路的coverage报告功能覆盖率卡在83%怎么都上不去随机回归跑了几十个小时就是碰不到那几个边界组合。有人随口说了一句“要是能直接让工具自己枚举出所有能触发这个状态的情况就好了。”当时没当回事后来我接触到符号仿真symbolic simulation和符号testbench才明白那句话其实就是验证领域里一个被长期低估的方向用符号化的方式把“验证意图”直接交给工具去求解而不是靠人去猜测激励。所谓的符号testbench简单说就是不把testbench输入限定成一个具体的0/1序列而是把输入当作一个符号变量让形式化工具在符号空间里自动搜索满足条件的激励。你不用写几百条SVA来覆盖各种场景你只要表达清楚“我要验证什么”剩下的路径探索交给求解器。这种思路适合那些条件组合多、边界深、随机仿真很难自动踩中的验证场景是SVA之外的另一种思路而且它和你用SVA做的检查并不冲突两者是互补关系。这篇文章我想分享的是符号testbench到底是什么、它的验证意图是怎么表达的、和SVA的差异在哪里以及怎么在一个真实的RTL模块上把它跑起来。我会尽量讲得具体一些包括工具链、代码示例、参数设置和踩过的坑希望给正在为验证覆盖率发愁的工程师多一个可以落地的选项。2. 符号testbench的思维转换从“条件声明”到“存在性搜索”2.1 SVA表达的是“在什么条件下必须怎么样”符号testbench表达的是“什么条件下会发生什么”先理清楚SVA的本质。SVA写的断言本质上是一个线性时序逻辑公式。assert property ((posedge clk) a |- b);这句话的意思是当a在当前拍为真时下一拍b必须为真。这是对设计行为的一种“法规性约束”。验证工程师做的就是不停地往testbench里注入激励让仿真器去检查这些法规是否被违反。SVA的质量高度依赖于你写属性时对场景的理解程度也就是说你得先想清楚什么情况下设计应该有怎样的表现然后把这个“什么情况”固化到穷举条件里。但在很多复杂场景里验证意图恰恰不是“某个条件下的行为”而是“设计是否存在一个状态使得某个条件可达”。比如FIFO在写读指针交错到一定程度时是否存在一个序列可以让空/满标志同时出错总线上是否存在一个合法的仲裁序列使某条请求永远得不到grant对于一个有限状态机是否存在一条不经过IDLE状态的路径能直接从状态A到状态C这些问题本质上都是状态空间的可达性问题而不是断言式约束。用SVA写可达性检查你得先把路径枚举出来这往往是不可行的因为状态空间太大人的脑力不够用。符号testbench的思路则完全不同它把输入信号当成符号把设计的状态转移逻辑当作约束用求解器去问“这样一组输入是否存在”。验证意图在这里发生了变化不是“检查行为是否违反规则”而是“搜索解空间里是否存在满足规则的激励”。我画个不精确但很好懂的类比。SVA像交警在路口盯着监控看有没有车闯红灯。符号testbench则像交通规划部门问有没有可能存在一种车流组合让某个路口在早高峰彻底锁死前者是规则检查后者是可达性分析两个问题可以同时回答。2.2 符号变量、约束求解器与反例的根本区别要理解符号testbench得先接受三个基本概念。第一符号变量。传统testbench里输入信号的每一个bit在仿真的某一时刻都有确定的0或1符号testbench里输入信号的bit可以是一个“符号”它没有被赋值只是一个抽象的布尔变量。仿真器在做符号执行时会把这些符号变量带进逻辑计算里跑出来的结果也是一个由这些符号变量构成的布尔表达式。比如说你给一个2输入与门输入a是符号变量x输入b是符号变量y那么输出就是xy而不是一个具体的值。第二约束求解器。符号仿真跑完一轮之后你会得到一个布尔表达式它表示“在什么条件下目标信号会变成某个值”。接下来让约束求解器比如Z3、Boolector去判断这个表达式是否可满足SAT/UIO/SMT。如果可满足求解器会给你一组具体的符号赋值这就是一条能触发目标条件的实际激励如果不可满足就说明在给定的约束空间里不存在这样的激励。第三反例Counterexample。符号testbench返回的“能触发条件的激励”在验证的意义上其实就是一个反例如果这个条件本身是你期望永远不会发生的比如assertion的违反那这个反例就帮你证明设计存在bug如果这个条件是你希望发生的比如覆盖率目标那这个反例就变成了一段可用于动态仿真的测试向量。整个过程听起来挺玄但其实你不需要自己实现符号引擎。目前主流的方法是用开源工具Yosys把RTL综合成门级网表再用SymbiYosyssby配合SAT/SMT求解器来做符号模型检验model checking。符号testbench在sby里可以直接用formal指令来跑也可以用cover指令来搜索可达状态两种模式下testbench的写法和普通Verilog颇为不同。2.3 验证意图在三种层面的表达形式我自己的体会是符号testbench中的“验证意图”不一定非要写成一条条断言它可以落到三个层面。第一个层面是断言的可达性。你依然可以写SVA属性但不同的是符号testbench不是随机跑仿真去验证属性而是用形式化引擎去证明在给定深度比如N个周期内这个属性是否在所有可能的输入下都成立。如果不成立引擎直接返回反例。这就是大家常说的“用形式化验证formal verification做断言检查”。符号testbench在这里的价值是把原来需要跑几百万次随机回归的验证意图压缩成一个可满足性问题。第二个层面是覆盖的引导性。Functional coverage声明了你想看的功能点比如“写指针和读指针相差恰好等于FIFO深度减1”。在随机仿真里这个条件可能很难自动碰上但在符号testbench里你只要把它写成一条cover属性引擎就会搜索是否存在一个激励序列能到达这个状态。如果能找到反例本身就是一条高效的定向激励直接拿到动态仿真里用覆盖率的收敛速度能提升非常明显。第三个层面是模型条件的目的性假设。这是最灵活的一种用法。你可以在testbench里先给设计加一些假设约束assume比如“复位释放后至少经过5拍才允许进行第一次写操作”然后在这种约束下问引擎是否存在一个合法激励让某个内部状态触发一个危险情况这种做法本质上就是把“验证意图”从顶层接口下放到模块内部状态你在符号testbench里关心的问题比写SVA时更接近设计本身的边界条件。3. 核心实操用SymbiYosys搭建第一个符号testbench3.1 工具链选型为什么我推荐Yosys sby聊工具之前先交代背景。工业界的商业形式化验证工具性能确实很强但授权门槛高想快速验证一个思路不太现实。开源这边Yosys作为RTL综合工具已经很成熟它不只是做逻辑综合还支持将Verilog转成形式化验证用的门级网表和属性逻辑。SymbiYosys简称sby是Yosys周边的一个形式化验证前端它把Yosys综合、求解器调用、断言检查、覆盖搜索这些环节串起来使用起来比直接写底层接口方便很多。我用的是Yosys 0.33 sby 0.32版本求解器默认配了Z3和Boolector。安装方式在Ubuntu上很直接sudo apt install yosys sudo apt install sby sudo apt install z3如果是其他平台也可以直接从GitHub拉源码编译。这里多提一句sby对Boolector和Z3的适配度都很高但实际使用下来Z3在涉及算术运算的场景比如计数器、地址加减中表现更好Boolector在纯逻辑布尔运算中更快。如果你要验证的模块里满是乘加器强烈建议把求解器换成Z3否则求解时间可能让人崩溃。写符号testbench的时候工程目录结构我习惯这样组织symbolic_verify/ ├── rtl/ │ └── counter.v ├── tb/ │ └── formal_tb.sv └── sby/ └── counter_cover.sbyrtl放设计源码tb放符号testbench文件sby放验证配置。这是一个很基础的结构却是后续所有实验的骨架。3.2 写一个可复现的例子可变起始值计数器的覆盖搜索为了把前面的概念落到具体代码里我用一个非常经典的模块来做演示一个可配置起始值的计数器。功能很简单输入clk、rst_n、load_en、load_value[7:0]、count_en复位后计数值为0当load_en为高时计数值装载为load_value当count_en为高时计数值在每个时钟周期加1输出overflow_flag在计数值达到255后再加1时拉高一个周期。代码写出来大概是这样module counter ( input clk, input rst_n, input load_en, input [7:0] load_value, input count_en, output reg overflow_flag ); reg [7:0] count; always (posedge clk or negedge rst_n) begin if (!rst_n) begin count 8h00; overflow_flag 1b0; end else if (load_en) begin count load_value; overflow_flag 1b0; end else if (count_en) begin {overflow_flag, count} {1b0, count} 9h1; end else begin overflow_flag 1b0; end end endmodule传统testbench会怎么做给load_value赋值几组边界值0、127、255再让count_en拉高几百个周期看overflow_flag是否在正确的周期数后出现。但这样验证有个明显盲区你无法穷举所有load_value和所有count_en序列的组合。如果load_value是某个中间值且count_en时断时续到底能不能在某个周期触发溢出随机仿真可能永远跑不到这个组合。在符号testbench里我不指定load_value的具体值而是把它当作符号变量。为了给求解器合理的搜索范围我可以加约束load_value只取奇数。然后我要搜索的问题是是否存在一个合法的激励序列使得overflow_flag在复位后第N个周期拉高这个问题用SVA写非常繁琐但在sby里只需要在testbench中写一条cover属性。注意这里有个关键点符号testbench文件并不是一个可综合的testbench它是专门为形式化验证写的“formal testbench”里面的接口、约束、属性都带上了形式化验证的标签。我的formal_tb.sv内容如下module formal_tb ( input clk, input rst_n ); reg [7:0] load_value; reg load_en; reg count_en; reg overflow_flag; // 将DUT实例化 counter dut ( .clk (clk), .rst_n (rst_n), .load_en (load_en), .load_value (load_value), .count_en (count_en), .overflow_flag (overflow_flag) ); // 符号testbench的关键把分析目标交给verify指令 // 这里我们使用sby的formal模式默认所有输入都是符号变量 // 也可以显式声明符号输入范围 // 给load_value添加约束只允许奇数 assume property (load_value[0] 1b1); // 复位释放后至少等待2拍再开始装载 reg [2:0] post_rst_cnt; always (posedge clk or negedge rst_n) begin if (!rst_n) post_rst_cnt 3b0; else if (post_rst_cnt 3d4) post_rst_cnt post_rst_cnt 1b1; end // 只允许复位释放4拍后拉高load_en assume property (post_rst_cnt 3d4 || !load_en); // 目标在第5拍(复位释放后)到第8拍之间overflow_flag至少为高一次 cover property ( post_rst_cnt 3d4 post_rst_cnt 3d8 overflow_flag 1b1 ) ; endmodule这里assume property用来给符号输入加约束cover property用来声明验证意图“我想找到一个激励让overflow_flag在指定区间出现”。在symbolic模式下sby会把load_value、load_en、count_en都当作符号变量去枚举。有一点必须强调symbolic testbench中的cover不是动态仿真里的coverage收集它是给求解器一个“目标命题”让引擎去寻找使它成立的输入序列。如果引擎回答“可满足”它会返回一个反例波形里面就包含了具体的load_value和count_en序列如果回答“不可满足”说明在当前约束下这个意图无法实现。3.3 sby配置文件的参数解读与求解器选择有了testbench下一步是写sby配置文件。我的counter_cover.sby长这样[options] mode cover depth 12 skip 4 [engines] smtbmc z3 [script] read_verilog -formal rtl/counter.v read_verilog -formal tb/formal_tb.sv prep -top formal_tb [files] rtl/counter.v tb/formal_tb.sv逐个参数解释一下。mode cover告诉sby这次跑的是覆盖搜索任务而不是断言证明任务mode prove。两者算法上略有区别cover更偏向搜索prove更偏向证明不变量。depth 12这是符号展开的时间深度单位是时钟周期。它决定了引擎最多往后搜索多少个周期。这个值要根据设计复杂度来定如果设小了目标状态可能还没达到就停下了设大了求解时间会指数级增长。对于这个简单计数器12拍足够覆盖装载后的计数行为。skip 4表示跳过前4个周期不做覆盖检查主要用来跳过复位和复位释放初期的非稳态区域。这个值要和testbench里假设约束的时序对齐。engines一项我用了smtbmc z3。smtbmc是sby内置的符号模型检查引擎配合Z3求解器适合处理含算术逻辑的电路。如果模块纯逻辑、没有复杂运算也可以换成btormc boolector通常更快。这里给出一个经验性的选型表设计特点推荐引擎/求解器备注纯组合逻辑为主btm cor求解速度快资源消耗低计数器、地址加减等算术较多smtbmc z3算术求解能力强大规模状态机smtbmc yicesyices对位向量支持好混合算术与状态smtbmc z3通用性最强我在实际使用中倾向于无脑上Z3因为不同case之间切换求解器的成本远高于单个case多跑几分钟的成本。3.4 跑通之后怎么读懂反例波形配置写好后在sby目录下执行sby -f counter_cover.sby如果一切正常输出里会看到类似Status: PASS或者Status: FAIL。在cover模式下PASS意味着引擎找到了至少一个满足cover属性的激励如果不可满足才会显示FAIL。找到反例后sby会在counter_cover/engine_0/trace.vcd生成波形文件。第一次跑通这个流程的时候我其实挺惊讶的。Z3返回的反例里load_value是一个7位的具体值比如8b01010101而load_en和count_en的序列在几个周期内也是确定的。也就是说符号引擎花了几秒钟帮我找到了一段之前随机回归跑了很久都未必能碰到的激励组合。把这段VCD对应的输入序列提取出来回到动态仿真里重新播放覆盖率点上那几条边界路径很快就闭合了。把反例波形变成可回归的测试向量这一步本身也很有价值。sby生成的VCD可以直接用vpi或者read_vcd的流程读入测试平台但更简单粗暴的办法是直接把trace里显示出的输入值手写进一个task里。对于自动化程度要求高的团队可以考虑把它们转化成UVM序列。不过这个转化逻辑并不复杂最核心的难点其实在于怎么把反例波形里的输入时序准确提取出来我一般会用GTKWave打开VCD定位到目标信号拉高的那一段往前回溯三四个周期把输入序列记下来。别小看这个手工作业对于一次性验证意图来说足够用了。4. 符号testbench和SVA的协作谁在什么场景下更管用4.1 符号testbench适合解决的问题类型踩过不少坑之后我总结出符号testbench最适合的几类场景供大家参考。第一类是复杂配置寄存器空间的穿透性验证。SOC验证里经常有几十个配置寄存器不同的寄存器组合会影响模块的工作模式。传统方法靠UVM寄存器模型和随机序列去覆盖组合空间但组合爆炸导致覆盖率常年不达标。符号testbench可以直接把配置寄存器当作符号变量一次性搜索出“哪些配置组合能触发某条内部路径”效率比随机配置高一个量级。第二类是深边界状态的可达性分析。比如一个状态机有几十个状态从复位开始到某个特定状态可能需要经历一串非常特殊的事件序列。这种序列靠人肉写SVA很难cover全面但符号testbench天然适合把“到达状态X”写成cover属性让引擎去搜路径。第三类是协议时序的破缺检查。总线协议中某些非法场景的发生条件比如读请求和写请求在同一周期到达可能因为仲裁器的调度而难以触发。符号testbench里你直接把非法条件定义为cover属性如果引擎找到了反例这就意味着设计中存在一条能够产生非法状态的合法输入路径——不管它最后会不会被更高层的防护机制拦住这个反例本身对验证团队来说就是极有价值的信息。4.2 SVA仍是不可替代的两者协作才完整写到这里必须给SVA正名。符号testbench虽然有搜索能力但它不适合做连续、大规模的协议行为监控。比如一个AXI总线接口的握手时序在动态仿真里每个时钟周期都有可能出现新的传输你不可能为每笔传输都启动一次符号搜索。SVA的优势在于它和动态仿真深度绑定可以在跑大规模随机回归时实时报告违规位置。所以我的真实项目里的做法是用SVA搭日常回归的守夜人用符号testbench打覆盖收敛的攻坚仗。SVA负责把已知的、可枚举的协议规则变成库反复执行符号testbench负责把未知的、需要搜索的边界条件变成问题按需求解。两者并不冲突甚至会有一种奇妙的互补符号testbench中发现的反例往往会让你意识到一个新的SVA属性漏写了而SVA中反复出现的违规点也经常会成为下一个符号testbench搜索的目标。记得有一次我在一个AHB转APB桥的设计里先用SVA写好了完整的握手属性动态回归也很干净。但用了符号testbench之后引擎很快找到了一条路径在master连续back-to-back传输的情况下桥内部的一个中间状态可以在一个周期内被“跳过”导致总线响应优先级错误。这条路径在随机回归里从来没出现过但一旦把反例导入动态仿真挂上那条手写SVA错误立刻暴露。这个案例给我留下的印象很深SVA说的是“如果发生这个就必须那样”符号testbench回答的是“其实这个也可能会发生”。两者缺一不可。4.3 覆盖率收敛流程中的实操建议如果你打算在团队里落地符号testbench我的建议是不要一上来就追求全模块形式化验证那样工程量大、风险高。更稳妥的路径是从覆盖率最差的功能点入手把那些长期不收敛的点列出来针对每一个功能点写一个独立的符号testbench和对应的cover属性用sby跑搜索拿到反例把反例转成定向测试向量加入回归集跑回归确认覆盖率确实提升再考虑扩大搜索范围。这套流程最看重的是“小而精”。一个符号testbench只需覆盖一个验证意图跑起来快调试也容易不会因为设计复杂度过大而让求解器超时。等团队积累了一定的经验再逐步扩展搜索的深度和规模会稳得多。5. 常见问题与排查技巧实录5.1 求解器超时深度是最大的敌人形式化验证领域有一句话叫“state space explosion”状态空间爆炸。符号testbench最常见的失败形式就是求解器跑了几十分钟甚至几个小时都没有返回结果。大部分情况下罪魁祸首是depth设置过大。求解器需要展开N个周期的电路逻辑展开的逻辑深度越大求解的复杂度呈指数增长。我的习惯是先用一个很小的depth比如4快速验证testbench本身没有语法错误、约束没有冲突然后逐步增加depth每加一档都记录求解时间。如果depth从10加到11时求解时间暴涨说明这个设计的状态空间可能很复杂与其盲目加大depth不如想办法通过增加约束来“切小”搜索空间。比如计数器例子里的“只允许奇数load_value”就是把搜索空间剪枝了一半求解时间立刻下降。约束是符号testbench的利器善用约束可以解决大部分超时问题。5.2 assume写过头意图被约束“绑死”另一类很常见的问题是我称之为“假不可满足”。你以为cover属性怎么都搜不到反例实际上是因为assume property添加的约束过紧把可能的路径全部剪掉了。比如你在测试总线时assume里写道“master_ready信号永远为高”那如果设计里恰好有一段功能依赖ready拉低后的处理路径这条路径就永远不可能被搜索到了。排查这类问题有一个很实用的方法在sby输出里查看求解器内部的可满足性统计。如果Status: FAIL出现得很干脆求解时间很快那多半不是状态爆炸而是约束把空间给堵死了。这时候把assume先放开一轮或者直接在测试里注释掉部分约束再跑一次看看cover属性是否变成可满足。如果是那就说明你的约束定义和真实场景不符需要重新调整。5.3 VCD波形凌乱善用skip参数和控制信号反例波形刚导出来的时候往往包含前几个周期的非稳定状态。如果不加处理直接看会让人一头雾水。skip参数就是为了跳过这些垃圾窗口的。但有时候skip设得太大会错过关键事件发生的起点所以建议在设置skip时参照你testbench里的复位释放逻辑让跳过周期数略大于复位释放延迟保留一小段“启动余量”即可。调试时还有一个心法在符号testbench里尽量多保留一些“可观测状态”。比如把DUT内部的关键计数器、状态寄存器连接到testbench的wire上这样VCD里就会记录这些内部信号的演化过程。符号testbench虽然核心是求解但最终人要看懂反例还是离不开内部状态的变化轨迹。没有内部信号的VCD就像看一场没有表情的默剧很难理解引擎给出的结论为什么成立。5.4 与动态仿真回归的衔接问题最后再讲一个工程化的坑。符号testbench返回的反例是一段带具体时序的输入序列但它和UVM环境里的sequence结构差距往往很大。直接手写映射很容易出错而且反例多了以后维护成本很高。我的做法是写一个小的解析脚本读入sby生成的VCD输出成一份CSV表格每一列是一个输入信号每一行是一个时钟周期的取值然后在UVM环境里用一个通用的task drive_from_csv来驱动DUT。这样符号testbench产生的反例可以直接变成动态回归的用例中间不需要手动干预。这个流程自动化之后团队里其他工程师使用符号testbench的门槛也大大降低了。他们不需要完全理解形式化验证的原理只需要提交一个验证意图拿回一条可回归的用例然后看覆盖率是否变化。对一个验证团队来说这才是新方法真正落地的前提。我在实际项目里体会到符号testbench最大的价值不在于替代SVA而在于它提供了一种新的提问方式。SVA让我们能表达“设计必须满足什么”符号testbench让我们能表达“设计是否有可能出现什么”。第一种问题适合日常回归第二种问题适合深挖边界。两种验证意图结合起来验证的完整性才会更高。这个方向的开源工具链虽然还没有商业工具那么顺手但已经足够支撑日常的验证攻坚了。如果你也遇到覆盖率收敛慢、回归找不到深层问题的情况不妨抽一个周末用Yosys和sby搭一个小例子试试。很可能你第一次跑通反例的时候就会理解我说的“另一种验证意图表达方式”到底是什么意思了。 符号testbench与SVA互补：用Yosys+SymbiYosys实现覆盖收敛新思路
1. 验证意图SVA并不是唯一答案做芯片验证这些年我一直有个感受SVASystemVerilog Assertions几乎成了“表达验证意图”的代名词。不管是协议检查、时序约束还是覆盖率收集大家都习惯性地用断言去描述“设计必须满足什么”。SVA也确实好用尤其在动态仿真里一条断言挂在接口上跑回归的时候就能实时盯着关键时序发现问题直接报错效率很高。但SVA也有它力不从心的时候。举一个很常见的例子你想验证一个计数器在任意起始值、任意使能序列下最终能否在10个周期内输出一个溢出标志。用SVA写你只能写“如果使能连续拉高10拍则溢出信号在第10拍拉高”这种带限定前缀的属性可一旦使能不是连续的、起始值不是0这类基于确定场景的断言就覆盖不了。你真正想问的问题是“有没有可能在某些输入序列下设计会进入某个特定状态”换句话说你想验证的不是“给定激励的结果”而是“激励空间里是否存在一条路径能到达某个条件”。这个问题SVA表达起来很别扭。我第一次意识到这个问题是在一次覆盖率收敛会上。团队拿着一个数据通路的coverage报告功能覆盖率卡在83%怎么都上不去随机回归跑了几十个小时就是碰不到那几个边界组合。有人随口说了一句“要是能直接让工具自己枚举出所有能触发这个状态的情况就好了。”当时没当回事后来我接触到符号仿真symbolic simulation和符号testbench才明白那句话其实就是验证领域里一个被长期低估的方向用符号化的方式把“验证意图”直接交给工具去求解而不是靠人去猜测激励。所谓的符号testbench简单说就是不把testbench输入限定成一个具体的0/1序列而是把输入当作一个符号变量让形式化工具在符号空间里自动搜索满足条件的激励。你不用写几百条SVA来覆盖各种场景你只要表达清楚“我要验证什么”剩下的路径探索交给求解器。这种思路适合那些条件组合多、边界深、随机仿真很难自动踩中的验证场景是SVA之外的另一种思路而且它和你用SVA做的检查并不冲突两者是互补关系。这篇文章我想分享的是符号testbench到底是什么、它的验证意图是怎么表达的、和SVA的差异在哪里以及怎么在一个真实的RTL模块上把它跑起来。我会尽量讲得具体一些包括工具链、代码示例、参数设置和踩过的坑希望给正在为验证覆盖率发愁的工程师多一个可以落地的选项。2. 符号testbench的思维转换从“条件声明”到“存在性搜索”2.1 SVA表达的是“在什么条件下必须怎么样”符号testbench表达的是“什么条件下会发生什么”先理清楚SVA的本质。SVA写的断言本质上是一个线性时序逻辑公式。assert property ((posedge clk) a |- b);这句话的意思是当a在当前拍为真时下一拍b必须为真。这是对设计行为的一种“法规性约束”。验证工程师做的就是不停地往testbench里注入激励让仿真器去检查这些法规是否被违反。SVA的质量高度依赖于你写属性时对场景的理解程度也就是说你得先想清楚什么情况下设计应该有怎样的表现然后把这个“什么情况”固化到穷举条件里。但在很多复杂场景里验证意图恰恰不是“某个条件下的行为”而是“设计是否存在一个状态使得某个条件可达”。比如FIFO在写读指针交错到一定程度时是否存在一个序列可以让空/满标志同时出错总线上是否存在一个合法的仲裁序列使某条请求永远得不到grant对于一个有限状态机是否存在一条不经过IDLE状态的路径能直接从状态A到状态C这些问题本质上都是状态空间的可达性问题而不是断言式约束。用SVA写可达性检查你得先把路径枚举出来这往往是不可行的因为状态空间太大人的脑力不够用。符号testbench的思路则完全不同它把输入信号当成符号把设计的状态转移逻辑当作约束用求解器去问“这样一组输入是否存在”。验证意图在这里发生了变化不是“检查行为是否违反规则”而是“搜索解空间里是否存在满足规则的激励”。我画个不精确但很好懂的类比。SVA像交警在路口盯着监控看有没有车闯红灯。符号testbench则像交通规划部门问有没有可能存在一种车流组合让某个路口在早高峰彻底锁死前者是规则检查后者是可达性分析两个问题可以同时回答。2.2 符号变量、约束求解器与反例的根本区别要理解符号testbench得先接受三个基本概念。第一符号变量。传统testbench里输入信号的每一个bit在仿真的某一时刻都有确定的0或1符号testbench里输入信号的bit可以是一个“符号”它没有被赋值只是一个抽象的布尔变量。仿真器在做符号执行时会把这些符号变量带进逻辑计算里跑出来的结果也是一个由这些符号变量构成的布尔表达式。比如说你给一个2输入与门输入a是符号变量x输入b是符号变量y那么输出就是xy而不是一个具体的值。第二约束求解器。符号仿真跑完一轮之后你会得到一个布尔表达式它表示“在什么条件下目标信号会变成某个值”。接下来让约束求解器比如Z3、Boolector去判断这个表达式是否可满足SAT/UIO/SMT。如果可满足求解器会给你一组具体的符号赋值这就是一条能触发目标条件的实际激励如果不可满足就说明在给定的约束空间里不存在这样的激励。第三反例Counterexample。符号testbench返回的“能触发条件的激励”在验证的意义上其实就是一个反例如果这个条件本身是你期望永远不会发生的比如assertion的违反那这个反例就帮你证明设计存在bug如果这个条件是你希望发生的比如覆盖率目标那这个反例就变成了一段可用于动态仿真的测试向量。整个过程听起来挺玄但其实你不需要自己实现符号引擎。目前主流的方法是用开源工具Yosys把RTL综合成门级网表再用SymbiYosyssby配合SAT/SMT求解器来做符号模型检验model checking。符号testbench在sby里可以直接用formal指令来跑也可以用cover指令来搜索可达状态两种模式下testbench的写法和普通Verilog颇为不同。2.3 验证意图在三种层面的表达形式我自己的体会是符号testbench中的“验证意图”不一定非要写成一条条断言它可以落到三个层面。第一个层面是断言的可达性。你依然可以写SVA属性但不同的是符号testbench不是随机跑仿真去验证属性而是用形式化引擎去证明在给定深度比如N个周期内这个属性是否在所有可能的输入下都成立。如果不成立引擎直接返回反例。这就是大家常说的“用形式化验证formal verification做断言检查”。符号testbench在这里的价值是把原来需要跑几百万次随机回归的验证意图压缩成一个可满足性问题。第二个层面是覆盖的引导性。Functional coverage声明了你想看的功能点比如“写指针和读指针相差恰好等于FIFO深度减1”。在随机仿真里这个条件可能很难自动碰上但在符号testbench里你只要把它写成一条cover属性引擎就会搜索是否存在一个激励序列能到达这个状态。如果能找到反例本身就是一条高效的定向激励直接拿到动态仿真里用覆盖率的收敛速度能提升非常明显。第三个层面是模型条件的目的性假设。这是最灵活的一种用法。你可以在testbench里先给设计加一些假设约束assume比如“复位释放后至少经过5拍才允许进行第一次写操作”然后在这种约束下问引擎是否存在一个合法激励让某个内部状态触发一个危险情况这种做法本质上就是把“验证意图”从顶层接口下放到模块内部状态你在符号testbench里关心的问题比写SVA时更接近设计本身的边界条件。3. 核心实操用SymbiYosys搭建第一个符号testbench3.1 工具链选型为什么我推荐Yosys sby聊工具之前先交代背景。工业界的商业形式化验证工具性能确实很强但授权门槛高想快速验证一个思路不太现实。开源这边Yosys作为RTL综合工具已经很成熟它不只是做逻辑综合还支持将Verilog转成形式化验证用的门级网表和属性逻辑。SymbiYosys简称sby是Yosys周边的一个形式化验证前端它把Yosys综合、求解器调用、断言检查、覆盖搜索这些环节串起来使用起来比直接写底层接口方便很多。我用的是Yosys 0.33 sby 0.32版本求解器默认配了Z3和Boolector。安装方式在Ubuntu上很直接sudo apt install yosys sudo apt install sby sudo apt install z3如果是其他平台也可以直接从GitHub拉源码编译。这里多提一句sby对Boolector和Z3的适配度都很高但实际使用下来Z3在涉及算术运算的场景比如计数器、地址加减中表现更好Boolector在纯逻辑布尔运算中更快。如果你要验证的模块里满是乘加器强烈建议把求解器换成Z3否则求解时间可能让人崩溃。写符号testbench的时候工程目录结构我习惯这样组织symbolic_verify/ ├── rtl/ │ └── counter.v ├── tb/ │ └── formal_tb.sv └── sby/ └── counter_cover.sbyrtl放设计源码tb放符号testbench文件sby放验证配置。这是一个很基础的结构却是后续所有实验的骨架。3.2 写一个可复现的例子可变起始值计数器的覆盖搜索为了把前面的概念落到具体代码里我用一个非常经典的模块来做演示一个可配置起始值的计数器。功能很简单输入clk、rst_n、load_en、load_value[7:0]、count_en复位后计数值为0当load_en为高时计数值装载为load_value当count_en为高时计数值在每个时钟周期加1输出overflow_flag在计数值达到255后再加1时拉高一个周期。代码写出来大概是这样module counter ( input clk, input rst_n, input load_en, input [7:0] load_value, input count_en, output reg overflow_flag ); reg [7:0] count; always (posedge clk or negedge rst_n) begin if (!rst_n) begin count 8h00; overflow_flag 1b0; end else if (load_en) begin count load_value; overflow_flag 1b0; end else if (count_en) begin {overflow_flag, count} {1b0, count} 9h1; end else begin overflow_flag 1b0; end end endmodule传统testbench会怎么做给load_value赋值几组边界值0、127、255再让count_en拉高几百个周期看overflow_flag是否在正确的周期数后出现。但这样验证有个明显盲区你无法穷举所有load_value和所有count_en序列的组合。如果load_value是某个中间值且count_en时断时续到底能不能在某个周期触发溢出随机仿真可能永远跑不到这个组合。在符号testbench里我不指定load_value的具体值而是把它当作符号变量。为了给求解器合理的搜索范围我可以加约束load_value只取奇数。然后我要搜索的问题是是否存在一个合法的激励序列使得overflow_flag在复位后第N个周期拉高这个问题用SVA写非常繁琐但在sby里只需要在testbench中写一条cover属性。注意这里有个关键点符号testbench文件并不是一个可综合的testbench它是专门为形式化验证写的“formal testbench”里面的接口、约束、属性都带上了形式化验证的标签。我的formal_tb.sv内容如下module formal_tb ( input clk, input rst_n ); reg [7:0] load_value; reg load_en; reg count_en; reg overflow_flag; // 将DUT实例化 counter dut ( .clk (clk), .rst_n (rst_n), .load_en (load_en), .load_value (load_value), .count_en (count_en), .overflow_flag (overflow_flag) ); // 符号testbench的关键把分析目标交给verify指令 // 这里我们使用sby的formal模式默认所有输入都是符号变量 // 也可以显式声明符号输入范围 // 给load_value添加约束只允许奇数 assume property (load_value[0] 1b1); // 复位释放后至少等待2拍再开始装载 reg [2:0] post_rst_cnt; always (posedge clk or negedge rst_n) begin if (!rst_n) post_rst_cnt 3b0; else if (post_rst_cnt 3d4) post_rst_cnt post_rst_cnt 1b1; end // 只允许复位释放4拍后拉高load_en assume property (post_rst_cnt 3d4 || !load_en); // 目标在第5拍(复位释放后)到第8拍之间overflow_flag至少为高一次 cover property ( post_rst_cnt 3d4 post_rst_cnt 3d8 overflow_flag 1b1 ) ; endmodule这里assume property用来给符号输入加约束cover property用来声明验证意图“我想找到一个激励让overflow_flag在指定区间出现”。在symbolic模式下sby会把load_value、load_en、count_en都当作符号变量去枚举。有一点必须强调symbolic testbench中的cover不是动态仿真里的coverage收集它是给求解器一个“目标命题”让引擎去寻找使它成立的输入序列。如果引擎回答“可满足”它会返回一个反例波形里面就包含了具体的load_value和count_en序列如果回答“不可满足”说明在当前约束下这个意图无法实现。3.3 sby配置文件的参数解读与求解器选择有了testbench下一步是写sby配置文件。我的counter_cover.sby长这样[options] mode cover depth 12 skip 4 [engines] smtbmc z3 [script] read_verilog -formal rtl/counter.v read_verilog -formal tb/formal_tb.sv prep -top formal_tb [files] rtl/counter.v tb/formal_tb.sv逐个参数解释一下。mode cover告诉sby这次跑的是覆盖搜索任务而不是断言证明任务mode prove。两者算法上略有区别cover更偏向搜索prove更偏向证明不变量。depth 12这是符号展开的时间深度单位是时钟周期。它决定了引擎最多往后搜索多少个周期。这个值要根据设计复杂度来定如果设小了目标状态可能还没达到就停下了设大了求解时间会指数级增长。对于这个简单计数器12拍足够覆盖装载后的计数行为。skip 4表示跳过前4个周期不做覆盖检查主要用来跳过复位和复位释放初期的非稳态区域。这个值要和testbench里假设约束的时序对齐。engines一项我用了smtbmc z3。smtbmc是sby内置的符号模型检查引擎配合Z3求解器适合处理含算术逻辑的电路。如果模块纯逻辑、没有复杂运算也可以换成btormc boolector通常更快。这里给出一个经验性的选型表设计特点推荐引擎/求解器备注纯组合逻辑为主btm cor求解速度快资源消耗低计数器、地址加减等算术较多smtbmc z3算术求解能力强大规模状态机smtbmc yicesyices对位向量支持好混合算术与状态smtbmc z3通用性最强我在实际使用中倾向于无脑上Z3因为不同case之间切换求解器的成本远高于单个case多跑几分钟的成本。3.4 跑通之后怎么读懂反例波形配置写好后在sby目录下执行sby -f counter_cover.sby如果一切正常输出里会看到类似Status: PASS或者Status: FAIL。在cover模式下PASS意味着引擎找到了至少一个满足cover属性的激励如果不可满足才会显示FAIL。找到反例后sby会在counter_cover/engine_0/trace.vcd生成波形文件。第一次跑通这个流程的时候我其实挺惊讶的。Z3返回的反例里load_value是一个7位的具体值比如8b01010101而load_en和count_en的序列在几个周期内也是确定的。也就是说符号引擎花了几秒钟帮我找到了一段之前随机回归跑了很久都未必能碰到的激励组合。把这段VCD对应的输入序列提取出来回到动态仿真里重新播放覆盖率点上那几条边界路径很快就闭合了。把反例波形变成可回归的测试向量这一步本身也很有价值。sby生成的VCD可以直接用vpi或者read_vcd的流程读入测试平台但更简单粗暴的办法是直接把trace里显示出的输入值手写进一个task里。对于自动化程度要求高的团队可以考虑把它们转化成UVM序列。不过这个转化逻辑并不复杂最核心的难点其实在于怎么把反例波形里的输入时序准确提取出来我一般会用GTKWave打开VCD定位到目标信号拉高的那一段往前回溯三四个周期把输入序列记下来。别小看这个手工作业对于一次性验证意图来说足够用了。4. 符号testbench和SVA的协作谁在什么场景下更管用4.1 符号testbench适合解决的问题类型踩过不少坑之后我总结出符号testbench最适合的几类场景供大家参考。第一类是复杂配置寄存器空间的穿透性验证。SOC验证里经常有几十个配置寄存器不同的寄存器组合会影响模块的工作模式。传统方法靠UVM寄存器模型和随机序列去覆盖组合空间但组合爆炸导致覆盖率常年不达标。符号testbench可以直接把配置寄存器当作符号变量一次性搜索出“哪些配置组合能触发某条内部路径”效率比随机配置高一个量级。第二类是深边界状态的可达性分析。比如一个状态机有几十个状态从复位开始到某个特定状态可能需要经历一串非常特殊的事件序列。这种序列靠人肉写SVA很难cover全面但符号testbench天然适合把“到达状态X”写成cover属性让引擎去搜路径。第三类是协议时序的破缺检查。总线协议中某些非法场景的发生条件比如读请求和写请求在同一周期到达可能因为仲裁器的调度而难以触发。符号testbench里你直接把非法条件定义为cover属性如果引擎找到了反例这就意味着设计中存在一条能够产生非法状态的合法输入路径——不管它最后会不会被更高层的防护机制拦住这个反例本身对验证团队来说就是极有价值的信息。4.2 SVA仍是不可替代的两者协作才完整写到这里必须给SVA正名。符号testbench虽然有搜索能力但它不适合做连续、大规模的协议行为监控。比如一个AXI总线接口的握手时序在动态仿真里每个时钟周期都有可能出现新的传输你不可能为每笔传输都启动一次符号搜索。SVA的优势在于它和动态仿真深度绑定可以在跑大规模随机回归时实时报告违规位置。所以我的真实项目里的做法是用SVA搭日常回归的守夜人用符号testbench打覆盖收敛的攻坚仗。SVA负责把已知的、可枚举的协议规则变成库反复执行符号testbench负责把未知的、需要搜索的边界条件变成问题按需求解。两者并不冲突甚至会有一种奇妙的互补符号testbench中发现的反例往往会让你意识到一个新的SVA属性漏写了而SVA中反复出现的违规点也经常会成为下一个符号testbench搜索的目标。记得有一次我在一个AHB转APB桥的设计里先用SVA写好了完整的握手属性动态回归也很干净。但用了符号testbench之后引擎很快找到了一条路径在master连续back-to-back传输的情况下桥内部的一个中间状态可以在一个周期内被“跳过”导致总线响应优先级错误。这条路径在随机回归里从来没出现过但一旦把反例导入动态仿真挂上那条手写SVA错误立刻暴露。这个案例给我留下的印象很深SVA说的是“如果发生这个就必须那样”符号testbench回答的是“其实这个也可能会发生”。两者缺一不可。4.3 覆盖率收敛流程中的实操建议如果你打算在团队里落地符号testbench我的建议是不要一上来就追求全模块形式化验证那样工程量大、风险高。更稳妥的路径是从覆盖率最差的功能点入手把那些长期不收敛的点列出来针对每一个功能点写一个独立的符号testbench和对应的cover属性用sby跑搜索拿到反例把反例转成定向测试向量加入回归集跑回归确认覆盖率确实提升再考虑扩大搜索范围。这套流程最看重的是“小而精”。一个符号testbench只需覆盖一个验证意图跑起来快调试也容易不会因为设计复杂度过大而让求解器超时。等团队积累了一定的经验再逐步扩展搜索的深度和规模会稳得多。5. 常见问题与排查技巧实录5.1 求解器超时深度是最大的敌人形式化验证领域有一句话叫“state space explosion”状态空间爆炸。符号testbench最常见的失败形式就是求解器跑了几十分钟甚至几个小时都没有返回结果。大部分情况下罪魁祸首是depth设置过大。求解器需要展开N个周期的电路逻辑展开的逻辑深度越大求解的复杂度呈指数增长。我的习惯是先用一个很小的depth比如4快速验证testbench本身没有语法错误、约束没有冲突然后逐步增加depth每加一档都记录求解时间。如果depth从10加到11时求解时间暴涨说明这个设计的状态空间可能很复杂与其盲目加大depth不如想办法通过增加约束来“切小”搜索空间。比如计数器例子里的“只允许奇数load_value”就是把搜索空间剪枝了一半求解时间立刻下降。约束是符号testbench的利器善用约束可以解决大部分超时问题。5.2 assume写过头意图被约束“绑死”另一类很常见的问题是我称之为“假不可满足”。你以为cover属性怎么都搜不到反例实际上是因为assume property添加的约束过紧把可能的路径全部剪掉了。比如你在测试总线时assume里写道“master_ready信号永远为高”那如果设计里恰好有一段功能依赖ready拉低后的处理路径这条路径就永远不可能被搜索到了。排查这类问题有一个很实用的方法在sby输出里查看求解器内部的可满足性统计。如果Status: FAIL出现得很干脆求解时间很快那多半不是状态爆炸而是约束把空间给堵死了。这时候把assume先放开一轮或者直接在测试里注释掉部分约束再跑一次看看cover属性是否变成可满足。如果是那就说明你的约束定义和真实场景不符需要重新调整。5.3 VCD波形凌乱善用skip参数和控制信号反例波形刚导出来的时候往往包含前几个周期的非稳定状态。如果不加处理直接看会让人一头雾水。skip参数就是为了跳过这些垃圾窗口的。但有时候skip设得太大会错过关键事件发生的起点所以建议在设置skip时参照你testbench里的复位释放逻辑让跳过周期数略大于复位释放延迟保留一小段“启动余量”即可。调试时还有一个心法在符号testbench里尽量多保留一些“可观测状态”。比如把DUT内部的关键计数器、状态寄存器连接到testbench的wire上这样VCD里就会记录这些内部信号的演化过程。符号testbench虽然核心是求解但最终人要看懂反例还是离不开内部状态的变化轨迹。没有内部信号的VCD就像看一场没有表情的默剧很难理解引擎给出的结论为什么成立。5.4 与动态仿真回归的衔接问题最后再讲一个工程化的坑。符号testbench返回的反例是一段带具体时序的输入序列但它和UVM环境里的sequence结构差距往往很大。直接手写映射很容易出错而且反例多了以后维护成本很高。我的做法是写一个小的解析脚本读入sby生成的VCD输出成一份CSV表格每一列是一个输入信号每一行是一个时钟周期的取值然后在UVM环境里用一个通用的task drive_from_csv来驱动DUT。这样符号testbench产生的反例可以直接变成动态回归的用例中间不需要手动干预。这个流程自动化之后团队里其他工程师使用符号testbench的门槛也大大降低了。他们不需要完全理解形式化验证的原理只需要提交一个验证意图拿回一条可回归的用例然后看覆盖率是否变化。对一个验证团队来说这才是新方法真正落地的前提。我在实际项目里体会到符号testbench最大的价值不在于替代SVA而在于它提供了一种新的提问方式。SVA让我们能表达“设计必须满足什么”符号testbench让我们能表达“设计是否有可能出现什么”。第一种问题适合日常回归第二种问题适合深挖边界。两种验证意图结合起来验证的完整性才会更高。这个方向的开源工具链虽然还没有商业工具那么顺手但已经足够支撑日常的验证攻坚了。如果你也遇到覆盖率收敛慢、回归找不到深层问题的情况不妨抽一个周末用Yosys和sby搭一个小例子试试。很可能你第一次跑通反例的时候就会理解我说的“另一种验证意图表达方式”到底是什么意思了。