基于STG模型的半形式化验证:从穷举到智能覆盖的策略演进
1. 项目概述当功能验证遇上“大海捞针”在数字芯片设计的漫长流程里功能验证是确保设计正确性的最后一道也是最关键的一道防线。想象一下你设计了一个复杂的处理器或通信模块里面有成千上万个逻辑门和寄存器它们在不同的输入组合下会产生天文数字般的行为可能性。传统的仿真验证就像拿着手电筒在漆黑的迷宫里摸索你永远不知道下一个转角会错过什么。这就是为什么自动测试向量生成ATPG技术如此重要——它试图系统化地照亮这个迷宫。然而ATPG本身也面临着一个核心矛盾验证的完备性与验证效率之间的权衡。对于控制逻辑比如状态机我们可以相对容易地遍历所有状态和转移。但一旦涉及数据路径问题就变得棘手了。一个32位的整数输入其合法取值范围有40多亿种可能。如果设计中有多个这样的数据端口测试空间会迅速膨胀到无法穷举的程度。传统的约束随机验证CRV方法虽然能产生大量随机激励但就像漫无目的地撒网存在严重的冗余和覆盖不均问题导致验证强度在某些角落非常薄弱。我最近在复现和深入研究一篇关于“基于STG模型的半形式化功能验证”的论文时对其中的“测试空间覆盖策略”部分感触颇深。这个策略直击了数据敏感型转换验证的痛点。它没有试图去覆盖那不可能覆盖的“整个海洋”而是聪明地提出只要覆盖了所有“暗礁”角点案例并对“海域”随机案例进行有代表性的抽样就能达到“令人满意”的覆盖效果。这种思路将我们从“穷举”的思维定式中解放出来转向更务实、更高效的“智能采样”。接下来我将结合自己的实践经验详细拆解这套策略的核心思想、实现细节并分享在工具实现和应用中的一些心得与避坑指南。2. 核心思路拆解从“穷举”到“满意覆盖”的范式转变2.1 STG模型搭建验证的“导航图”要理解测试空间覆盖策略首先得明白它的载体——阶段转换图STG模型。你可以把STG看作是从设计规格说明书Specification中提炼出来的一张“行为导航图”。它不关心RTL代码里具体的寄存器传输级细节而是抽象出关键的功能点Function Point每个功能点被建模为一个STG。一个STG由“阶段Stage”和“转换Transition”构成。阶段代表设计在完成某个子功能时所处的稳定状态而转换则代表从一个阶段切换到另一个阶段所需满足的条件和动作。这里的关键在于转换的条件函数Condition Function会涉及设计的输入端口。根据端口影响的逻辑性质我们将其分为两类控制路径Control-Path端口通常位数较少取值离散且有限例如状态机的控制信号、操作码opcode等。其测试空间相对较小。数据路径Data-Path端口位数宽取值连续或范围巨大例如数据总线、地址、运算操作数等。这正是导致测试空间爆炸的元凶。基于STG的ATPG目标就是生成一系列输入向量驱动设计遍历这些STG中所有可能的路径阶段和转换。对于控制敏感型转换条件主要依赖控制路径端口由于其测试空间小我们可以追求完全覆盖。但对于数据敏感型转换条件主要依赖数据路径端口完全覆盖是天方夜谭必须采用新的策略。2.2 “满意覆盖”准则的提出论文提出的“满意覆盖Satisfying Coverage”准则是整套策略的基石。它承认无法覆盖数据敏感型转换的整个测试空间但定义了一个切实可行的目标完全覆盖所有角点案例Corner Cases这是必须达到的底线。角点案例通常是边界值、特殊值如0 最大值 最小值 溢出值等是设计最容易出错的场景。覆盖一定规模的随机案例Random Cases在角点覆盖的基础上还需要对广阔的“正常值”空间进行抽样以检测那些在常规边界外可能存在的隐藏缺陷。这个“一定规模”是可以由验证工程师根据验证进度和资源动态设定的。这个准则的精妙之处在于它将无限的覆盖问题转化为了一个“角点覆盖有限 空间抽样可控”的复合问题。角点分析确保“关键点”无一遗漏而测试空间分解则确保“面”上的抽样是均匀且高效的避免了传统CRV的盲目性。2.3 策略双引擎角点分析与空间分解为了实现“满意覆盖”论文配套了两大核心方法角点案例自动分析方法其核心洞察是数据路径端口的角点值与其数据类型强相关。例如对于一个有符号32位整数int32_t其角点值通常包括最小值-2^31、最大值2^31-1、0、以及可能接近溢出阈值的值如最大值-1 最小值1。该方法利用一个“专家知识库”为每种数据类型int8, uint16, float等预定义或学习其典型的角点值集合。当遇到一个数据敏感型转换时工具会自动提取其数据路径端口的数据类型从知识库中获取对应的角点值再与此时控制路径端口的所有合法取值进行组合从而自动生成覆盖所有角点的测试向量。测试空间分解方法这是解决随机覆盖均匀性的关键。传统CRV在整个大空间里随机撒点可能导致某些子区域被过度测试而另一些子区域被忽略。空间分解的思路是先将庞大的测试空间均匀地切割成若干个较小的子空间Subspace。然后在每一个子空间内分别进行随机采样。这样就能保证每个子空间都能获得“平等”的验证关注度。注意这里的“均匀”切割并非指数学上严格的等分对于复杂的数据类型和约束可能很难做到而是指一种基于取值范围的、逻辑上的划分。例如将一个32位无符号整数的取值范围 [0, 2^32-1] 简单地划分为 [0, 2^31-1] 和 [2^31, 2^32-1] 两个子空间就是一种最简单的分解。3. 核心细节解析与实操要点3.1 角点分析如何构建“专家知识库”角点分析方法的自动化程度高度依赖于“专家知识库”的完备性和智能性。在实际工具实现中这个知识库不能是静态的、死板的列表。1. 知识库的初始构建知识库需要内置对常见数据类型的角点值定义。这需要融合领域常识和设计经验整型Integer最小值MIN、最大值MAX、零0、全1~0、字节边界值如0xFF, 0xFFFF等。定点数Fixed-Point除了整型的角点还需考虑小数部分的溢出以及动态范围边界。浮点数Float正负零0.0, -0.0、正负无穷大inf, -inf、NaNNot a Number、规格化数的最大/最小值、次正规数Subnormal边界等。枚举/状态类型所有可能的枚举值。数组索引0首元素、长度-1末元素、以及可能越界的值如长度 或-1。2. 知识库的动态学习与扩展一个先进的工具应该支持知识库的演进。例如从约束中提取如果设计对输入有额外的约束通过SystemVerilog的randc、inside或constraint定义工具应能解析这些约束并将其边界值补充为角点。例如rand data inside {[100:200]};那么100和200就应被视为角点。从覆盖反馈中学习如果在历史验证中某些非典型值触发了缺陷工具可以允许工程师手动将这些值标记为“关键值”并加入知识库用于后续类似设计的验证。用户自定义提供接口让验证工程师为特定设计或模块添加自定义的角点值。实操心得在搭建或选用工具时一定要评估其角点知识库的灵活性和可扩展性。一个只能处理基本整型的工具在面对复杂DSP或AI加速器中的特殊数据类型如BF16浮点、块浮点数时会力不从心。最好的方式是工具提供基础库同时开放完善的API或配置文件让用户能够根据项目特点进行定制和丰富。3.2 测试空间分解数学原理与工程折衷论文中给出了一个简化的数学模型来说明空间分解的效率提升。假设整个测试空间大小为n传统随机覆盖达到高概率覆盖所需的向量数期望为O(n log n)。如果将空间均匀切成k份那么覆盖每个子空间所需的向量数期望约为O((n/k) log(n/k))总期望约为O(n log(n/k))。当k增大时所需总向量数会减少。但这只是理想情况。工程实践中需要面对几个关键问题1. 如何“均匀”分解对于单变量按数值范围等分是直观的。但对于多变量共同构成的测试空间情况复杂得多。例如一个转换的条件同时依赖于两个32位数据A和B。如果简单地将A的范围切成2份A1, A2B的范围切成2份B1, B2那么组合起来会得到4个子空间(A1, B1), (A1, B2), (A2, B1), (A2, B2)。这要求A和B在条件函数中是相对独立的。如果条件函数是A B那么这种基于独立范围的划分可能会导致某些子空间如A1, B2即A小B大根本不满足条件函数成为无效子空间浪费了验证资源。2. 分解粒度的选择子空间数量k是关键的调节旋钮。k太小分解效果不明显可能仍存在覆盖不均k太大会产生大量子空间管理开销和随机向量生成的开销会增加甚至可能因为子空间太小而失去了随机抽样的意义。论文提到可以由工程师设定或由工具根据测试空间大小自动决定。一个实用的启发式规则是确保每个子空间在完成角点覆盖后还能容纳至少数十到数百个有意义的随机测试点。3. 与约束随机验证CRV的协同空间分解不是取代CRV而是引导CRV。分解后的每个子空间内部仍然使用CRV来生成随机向量。但此时的随机约束被限定在了当前子空间的范围内。这相当于给CRV戴上了“指哪打哪”的瞄准镜大大提升了随机验证的针对性和均匀性。避坑指南在实际应用中不要盲目追求数学上的完美分解。首先应分析数据敏感型转换的条件函数。如果变量间存在强耦合关系如比较、算术运算应考虑使用更智能的分解策略例如基于条件函数本身来引导空间划分。例如对于条件A B可以沿着A - B 0这个边界平面来划分空间而不是独立划分A和B。这通常需要更复杂的约束求解器支持但能极大提升分解的有效性。4. 实操过程与核心环节实现4.1 工具链整合STG-Test的运作视图论文中提到了一个名为STG-Test的工具实现。我们可以构想一个类似的、可落地的半自动化验证流程。这个流程的核心是将STG模型、测试空间覆盖策略与现有的仿真环境无缝集成。1. 输入准备阶段STG建模使用工具提供的GUI或DSL领域特定语言根据设计规格Spec绘制或编写STG模型。需要明确定义每个阶段、转换、以及转换的条件函数关联到具体的设计输入端口。配置专家知识库检查并补充工具内置的数据类型角点定义。对于项目特有的数据结构需要添加自定义角点规则。设置验证参数针对每个数据敏感型转换或全局设定“满意覆盖”的目标即随机案例的规模例如“每个子空间至少生成100个随机向量”和测试空间分解的粒度例如“将每个宽数据端口的取值范围平均分为4份”。2. 测试生成与仿真执行阶段核心循环工具内部会运行一个ATPG引擎其工作流程可以细化如下对于每一个待验证的STG 1. 获取当前活跃阶段。 2. 列出所有从该阶段出发的未覆盖转换。 3. 对于每个转换 a. 判断转换类型控制敏感 / 数据敏感。 b. 如果是控制敏感转换求解条件函数生成能触发该转换的确定性的输入向量可能涉及约束求解。 c. 如果是数据敏感转换 i. **角点覆盖阶段**调用角点分析模块。根据条件函数中数据端口的数据类型从知识库获取角点值列表。将其与控制端口的合法值组合生成一组确定的角点测试向量。执行仿真验证角点。 ii. **随机覆盖阶段**调用测试空间分解模块。根据预设粒度对数据端口的取值空间进行划分生成多个子空间。 iii. **子空间遍历**对于每一个子空间 - 将当前转换的条件函数附加“输入端口值属于当前子空间”这一约束。 - 在此约束下运行CRV引擎生成指定数量的随机测试向量。 - 执行仿真。 4. 根据仿真结果DUV输出和状态判断转换是否成功触发并更新STG的覆盖状态阶段覆盖SC 转换覆盖TC。 5. 如果当前阶段所有转换尝试完毕或达到某种策略通过回溯Backjumping算法跳转到其他未充分探索的阶段。这个循环会一直进行直到达到用户设定的覆盖目标如所有STG的TC达到100%所有数据敏感转换的TSC达到“满意”级别或资源时间、计算力耗尽。3. 结果收集与分析阶段仿真报告记录所有执行的测试向量、触发的转换、以及DUV的响应。覆盖率报告这是最重要的输出。它需要包含传统代码覆盖率行覆盖、条件覆盖、分支覆盖、FSM状态/转移覆盖。这是验证质量的基线。STG功能覆盖率这是本方法的核心指标。阶段覆盖率SC%已遍历的阶段数 / 总阶段数。转换覆盖率TC%已成功触发的转换数 / 总转换数。测试空间覆盖率TSC%对于控制敏感转换是已覆盖的合法输入组合数 / 总组合数对于数据敏感转换是已覆盖角点 已覆盖的随机子空间 / 总角点 总子空间。这是一个更贴近设计意图的覆盖指标。波形文件VCD/FSDB用于调试失败用例。4.2 一个具体的例子乘法累加单元MAC的验证假设我们有一个乘法累加单元MAC其一个核心功能点是计算A * B C。我们可以为此功能点建立一个简单的STG阶段S_idle空闲状态等待计算指令。转换T_calc从S_idle触发。条件函数opcode MAC_OP A_valid B_valid C_valid。其中opcode是控制端口A,B,C是32位有符号整数数据端口。阶段S_busy计算进行中。转换T_done从S_busy触发。条件函数calc_done 1‘b1。完成后回到S_idle。T_calc是一个典型的数据敏感转换。opcode和*_valid信号是控制部分空间很小。但A,B,C每个都有2^32种可能组合空间巨大。应用测试空间覆盖策略角点分析工具从知识库得知int32_t的角点包括0x80000000(MIN),0x7FFFFFFF(MAX),0x00000000(0),0xFFFFFFFF(-1) 等。它会生成诸如(AMIN, BMAX, C0),(A0, B0, CMAX),(A-1, B1, CMIN)等组合并与合法的opcode和*_valid组合形成角点测试向量。这些用例专门测试溢出、零值相乘、符号位处理等边界场景。空间分解工具将A,B,C每个变量的32位空间各均匀分为4个区间例如按符号位和数值高位划分。这样会产生44464个子空间。工程师设定每个子空间内生成50个随机向量。执行工具首先运行所有角点向量。然后依次遍历64个子空间。在每个子空间内约束A, B, C的值分别落在对应的区间内然后随机生成50组向量进行仿真。这总共会产生 角点向量数 64 * 50 约三千多个测试向量。虽然相比总数微不足道但它系统性地覆盖了所有关键边界和整个取值空间的一个均匀采样其验证信心远高于单纯随机生成三千万个向量。5. 常见问题与排查技巧实录在实际应用这类方法时会遇到一些典型问题。以下是我从经验中总结的排查清单问题现象可能原因排查步骤与解决技巧角点用例仿真失败1. 专家知识库的角点值不符合该设计的具体约束。2. 角点值触发了设计规格中未明确定义的行为即“未定义行为”但检查器按某种预期检查导致失败。3. 设计本身在角点处存在Bug。1.检查约束首先确认生成的角点值是否违反了设计输入的任何显式约束例如通过SystemVerilogassert或assume定义的。工具应能读取并遵守这些约束。2.审查规格核对设计规格说明书确认该角点场景下的预期输出究竟是什么。可能需要与架构师或算法设计师澄清。3.隔离测试单独创建一个仅包含该角点输入的定向测试用调试器深入跟踪波形定位是功能错误还是验证环境检查器的错误。测试空间覆盖率TSC提升缓慢1. 空间分解粒度太粗子空间太大内部随机采样难以触发复杂条件。2. 数据端口间存在强非线性约束如A*B C导致很多子空间实际为无效空间没有合法解。3. ATPG的回溯Backjumping策略不够高效卡在了某些难以触发的转换上。1.调整分解策略尝试增加分解粒度更多的子空间或者改用基于条件引导的分解如果工具支持。2.分析约束使用约束求解器的调试功能查看在特定子空间下条件函数是否可能被满足。如果大量子空间无效需要考虑重新建模STG或将强耦合的变量合并考虑进行分解。3.审视STG模型检查是否某些转换的条件函数过于严苛或依赖于未正确建模的内部状态。简化模型或增加中间阶段可能有助于ATPG探索。工具运行时间远超预期1. 为每个子空间生成的随机向量数量设置过多。2. 仿真环境本身较慢而工具生成的向量序列化/通信开销大。3. 存在大量转换失败后的重试和回溯增加了计算开销。1.优化参数降低每个子空间的随机向量数优先保证角点覆盖和更广的子空间覆盖而非单个子空间内的深度随机。采用“自适应”策略对容易触发的转换减少随机数对难以触发的转换增加资源。2.优化集成确保工具与仿真器如VCS, Xcelium的接口高效例如使用共享内存、DPI-C调用等方式避免频繁的文件IO。3.设置超时与截止为每个转换的尝试设置时间或尝试次数上限避免ATPG引擎在不可能触发的转换上无限循环。STG功能覆盖率TC/SC达100%但代码覆盖率仍有缺口这是非常常见的情况也恰恰说明了功能覆盖率的价值。1.缺口分析仔细分析未覆盖的代码。它们很可能对应的是a)错误处理或异常路径这些路径在你的STG模型中没有被建模因为规格书可能只描述了正常功能。你需要补充对应的错误处理STG或阶段。b)实现细节代码例如某些性能优化逻辑、冗余电路、或特定的低功耗控制逻辑。这些可能不属于“功能点”但需要验证。此时需要补充额外的定向测试或使用传统的CRV来覆盖。c)不可达代码可能是遗留代码或防御性编程代码永远无法执行。需要与设计人员确认。并发功能点测试时出现资源冲突多个STG代表的并发功能点在仿真中同时尝试驱动同一硬件资源如寄存器、内存端口导致冲突和仿真错误。集成动态调度策略。论文中提到了一种基于优先级的动态调度策略。在实际中可以1.设置资源锁在STG模型中声明其访问的共享资源。调度器在分配测试向量时进行冲突检测和仲裁。2.优先级与公平性为每个STG设置初始优先级例如访问资源多的优先级低以最大化并发并引入“饥饿避免”机制长时间未调度的STG提升其优先级。3.序列化执行对于确实存在严格互斥的功能点在STG模型中将其定义为互斥由调度器安排串行执行。这套基于STG和测试空间覆盖策略的半形式化方法其最大优势在于将验证的注意力从无限的代码空间引导到了有限但关键的功能行为空间。它不能替代全面的代码覆盖率检查但能极大地提升在有限时间内对设计核心功能进行系统化、高强度验证的效率。尤其适合在项目早期针对新开发模块的功能正确性进行快速验证和迭代。当它与形式验证、基于断言的验证等方法结合使用时能构建起一个层次化、互补的强大验证体系。