基于阶段转换图（STG）的半形式化功能验证方法与实践

1. 项目概述从规范到实现的功能验证新思路在硬件设计领域功能验证是确保芯片或电路系统行为符合预期功能描述的关键环节其成本与时间消耗常常占到整个设计周期的70%以上。传统上工程师们主要依赖两种路径基于仿真的动态验证以及基于形式化方法的静态验证。仿真验证灵活、直观但本质上是一种抽样检查难以穷尽所有可能的输入组合和内部状态那些隐藏在复杂交互深处的“边角情况”往往成为漏网之鱼最终演变为流片后的致命缺陷。形式化验证如模型检验理论上可以穷尽所有可能的行为但其著名的“状态爆炸”问题使其在面对稍具规模的设计时便举步维艰对工程师的数学功底和工具使用技巧也提出了极高要求。正是在这种两难困境下半形式化验证方法应运而生它试图在仿真验证的工程友好性与形式化验证的逻辑完备性之间寻找一个平衡点。其核心思想是用一个形式化的模型来精确描述设计应有的行为然后基于这个模型来指导仿真测试向量的生成和检查。这样测试不再是盲目的随机漫步而是模型驱动下的有目的探索。然而现有的大多数半形式化方法存在一个根本性的局限它们的形式化模型是从设计的实现通常是RTL代码中提取的。这带来了几个棘手的问题首先模型复杂度与实现本身强相关可扩展性差其次验证变成了“实现与实现的比较”仍然需要一个“黄金模型”或断言来判定对错并未真正追溯到需求的源头——设计规范。本文要探讨的正是一种“回归本源”的验证思路基于阶段转换图模型的半形式化功能验证方法。它的核心创新在于直接以人类可读的设计规范Specification为起点构建一种名为“阶段转换图”的形式化模型。这个模型不关心RTL代码里具体的寄存器或状态机是如何实现的只关注规范中定义的功能点、其间的时序关系以及输入输出行为。然后基于这个STG模型驱动一套自动测试向量生成引擎系统性地遍历模型中的所有行为路径从而高效地触发设计中的边角情况验证其功能正确性。这种方法跳过了对实现细节的依赖将验证的锚点牢牢钉在了最初的设计需求上对于控制密集型如仲裁器、协议控制器和数据密集型如计算单元、数据通路设计都展现出了良好的适用性。2. STG模型架起规范与形式化之间的桥梁2.1 为什么需要STG传统模型的局限性在深入STG细节之前我们先看看为什么从规范直接建模是个难题以及为什么传统的状态机模型不太适用。设计规范通常使用自然语言或半形式化的时序图、表格来描述功能其特点是时序描述是“多周期粒度”的规范会说“在收到请求信号后经过2-5个时钟周期返回应答”而不会精确描述这中间每个周期每个内部寄存器的变化。关注外部可见行为规范定义的是输入激励与输出响应之间的关系以及少数关键内部寄存器如状态寄存器、配置寄存器的行为对大量仅用于实现逻辑的中间寄存器是隐去的。包含复杂的数据操作除了控制流规范还定义了大量的数据计算、比较和传输。传统的有限状态机或扩展有限状态机模型本质上是“状态中心”的。它们试图为设计的每一个内部状态建模。当从实现中提取时这尚且可行尽管状态空间可能爆炸。但当从规范出发时我们缺乏这些内部状态的明确定义强行构建FSM会引入大量未定义的、臆测的状态使得模型既不准确又无比复杂。此外FSM模型难以优雅地表达“2-5个周期”这种时序区间也不擅长处理复杂的数据路径操作。2.2 STG的核心定义与构成要素阶段转换图模型正是为了克服这些局限性而设计的。它不再试图捕捉每一个内部状态而是将一个完整的功能点的执行过程抽象为一系列阶段的转换。每个阶段代表功能执行中的一个逻辑步骤或时间片段转换则由条件、时序标记和反应动作构成。一个STG模型可以形式化地定义为一个五元组I, O, V, S, TI (输入符号集)对应设计的主要输入端口。每个输入i是一个元组id, width, type包含端口名、位宽和数据类型如bit, int, float。明确数据类型对于后续生成有意义的测试数据至关重要。O (输出符号集)对应设计的主要输出端口。每个输出o是id, width。V (局部变量集)用于描述规范中明确提及的、对验证者可见的内部寄存器如状态寄存器、计数器、配置寄存器。每个变量v是id, type, initial_value包含变量名、数据类型和初始值。这是连接规范中抽象描述与具体信号的关键。S (阶段集)功能点执行过程中的各个逻辑阶段。其中s0是初始阶段代表功能开始。T (转换集)阶段之间的转换关系是STG的核心。每个转换t是一个五元组Ct, st, st, βt, αtCt时序标记。表示从转换条件满足到其反应动作完成所经历的时钟周期数。它可以是一个具体值如##2也可以是一个范围如##[1:3]。这是STG能精确描述规范中时序关系的关键。st源阶段。st目标阶段。βt条件函数。一个从当前输入I和变量V的取值映射到布尔值{True, False}的函数。它定义了触发此转换需要满足的条件。αt反应函数。一个从当前输入I和变量V的取值映射到输出O和更新后变量V的函数。它定义了转换触发后输出什么值以及如何更新内部变量。2.3 一个生动的STG建模实例让我们通过一个简化的定点算术单元的功能点来具体感受STG。假设规范描述如下单元有输入in1,in2,cntr输出out以及两个控制寄存器a和b初始值为0。开始时若in1和in2均小于 2^16则在1个周期后将in1的值赋给寄存器a。然后检查a和b是否都等于1。若是则在2个周期后将ab的结果输出到out功能结束。若否即a和b不都为1则在1个周期后输出0到out。接着检查cntr是否为1。若是则在2个周期后将a-b的结果输出到out功能结束。若cntr为0则在1个周期后将in2的值赋给寄存器b然后跳回步骤2继续执行。根据此规范我们可以构建出如图1所示的STG模型。模型包含S0到S5六个阶段以及t0到t5六条转换。例如转换t0的条件是{in1 65536 in2 65536}反应是[a in1]时序标记是##1。转换t2的条件依赖于变量a和b({a1 b1})这是一个变量依赖型转换而t0的条件只依赖于输入in1和in2这是一个输入依赖型转换。这个区分对后续的测试生成策略有重要影响。图1一个功能点的STG示例此处为描述性文字实际论文中包含图示展示了S0到S5的阶段及连接它们的转换t0-t5并标注了条件和反应。这个STG模型精准地捕获了规范中的所有关键信息操作的顺序、条判断、数据赋值、循环以及精确到周期级的时序要求。它没有涉及任何具体的加法器或比较器如何实现完全站在规范的角度进行描述。实操心得STG建模的起点与边界在实际项目中开始STG建模前必须与系统架构师或算法工程师紧密协作明确“功能点”的粒度。一个功能点应该对应规范中一个相对独立、可测试的功能描述例如“完成一次DMA传输”、“执行一条特定指令”、“处理一个协议包”。切忌试图用一个庞大的STG描述整个芯片的所有行为而应将其分解为多个STG每个STG验证一个子功能。同时要谨慎定义变量集V只包含规范中明确提及或逻辑上必须可见的寄存器。随意添加内部实现寄存器会污染模型使其重新陷入实现细节的泥潭。3. 基于STG的自动化测试生成策略有了精确的STG模型下一步就是如何利用它来自动化地生成高质量的测试向量。目标是系统性地遍历STG中的所有行为并充分覆盖每个转换的测试空间从而触发设计实现中所有可能的边角情况。我们的ATPG方法采用多轮遍历的策略其核心流程如图2所示主要包括两个引擎转换遍历引擎和测试空间覆盖策略。图2ATPG方法流程流程描述1. 选择一个未被覆盖的STG2. 转换遍历引擎选择一条待触发的转换3. 测试空间覆盖策略生成对应测试向量4. 重复2-3步直至该STG的测试空间被完全覆盖5. 覆盖所有STG后结束。3.1 转换遍历引擎确保路径可达性转换遍历引擎的目标是确保STG中的每一条转换边至少被触发一次。这相当于要走过模型中的每一条路。我们采用一种分层递进的策略3.1.1 随机漫步快速覆盖主干道首先使用随机漫步算法。算法从初始阶段S0开始在当前阶段所有可触发的转换即条件函数在当前输入和变量值下为真中随机选择一条来执行然后进入下一阶段重复此过程直至到达最终阶段。这个过程成本低、速度快能覆盖STG中大部分容易触发的路径。在我们之前的算术单元例子中从S0开始随机为in1和in2赋值如100, 200以满足t0进入S1。在S1t1的条件(a!1 || b!1)很可能为真因为a刚被赋值为100因此随机漫步很可能选择t1进入S2然后根据cntr的值选择t4或t5最终完成一条执行路径。然而随机漫步是“短视”的它只关注当前阶段可立即触发的转换。对于那些条件苛刻、依赖于特定变量取值的转换如例子中的t2要求a1 b1随机漫步几乎不可能偶然满足其条件。这些“难触发”的转换就被遗漏了。3.1.2 控制依赖分析与改进的回跳算法攻克顽固堡垒为了触发这些被遗漏的变量依赖型转换我们需要更智能的方法。首先进行控制依赖分析。控制依赖存在于两条转换之间一条转换如t0设置了某个变量如a的值另一条转换如t2的使用了这个变量的值作为触发条件。我们分析STG找出所有这样的依赖关系并构建控制依赖路径。例如(a, t0, t2)表示变量a在t0被赋值并被t2使用。传统的回跳算法可以解决单变量依赖问题当发现一个未触发的转换t_miss依赖于变量v而v在之前的转换t_dep中被赋值算法可以“回跳”到t_dep的源阶段并尝试为t_dep生成特定的输入使得t_dep执行后变量v的值恰好能满足t_miss的条件。但我们的算术单元例子提出了一个更复杂的挑战t2同时依赖于变量a和b。传统回跳算法分别处理a和b的依赖路径(a, t0, t2)和(b, t4, t2)可能会在解决a的约束时破坏了b的约束或者反之导致无法同时满足两者。为此我们提出了改进的回跳算法。它的核心改进在于协同处理多变量依赖。算法不是孤立地处理每条依赖路径而是将它们合并考虑生成一条统一的回跳路径。这条回跳路径是包含所有相关控制依赖转换的最短执行序列。对于t2其回跳路径是t0 - t1 - t4 - t5。算法回跳到这条路径的起点S0然后沿着路径向前执行但不再是随机赋值而是求解一系列联合约束在S0触发t0时求解约束不仅要满足t0自身的条件(in165536 in265536)还要保证其反应(ain1)执行后a的值能满足t2对a的条件部分(a1)。即求解β_t0 (a in1) (a 1)。这迫使in1必须赋值为1。沿着路径经过t1到达S2后需要触发t4来设置b。同样求解约束满足t4的条件(cntr0)同时保证其反应(bin2)执行后b的值能满足t2对b的条件部分(b1)。即求解β_t4 (b in2) (b 1)。这迫使in2必须赋值为1且cntr为0。最终当执行回跳路径回到S1时变量a和b都已为1转换t2的条件自然满足得以触发。这种将多个变量的约束条件沿着一条精心规划的回跳路径进行传播和协同求解的策略极大地增强了对复杂依赖关系的处理能力能够确定性地触发那些多条件耦合的边角转换。3.2 测试空间覆盖策略追求深度而不仅是广度仅仅触发每条转换一次只是覆盖了功能的“广度”所有路径。但对于每一条转换其条件函数可能对应着一个庞大的输入取值空间测试空间。例如转换t0的条件是in165536 in265536合法的(in1, in2)组合有约2^32种。全覆盖显然不现实但我们需要一种策略来智能地采样以覆盖有代表性的情况特别是那些容易引发设计错误的“边角”值。我们的策略是根据转换中涉及的输入端口属性将转换分为两类并分别采用不同的覆盖策略3.2.1 控制敏感型转换的穷举覆盖如果一个转换的条件函数仅涉及控制路径端口如模式选择、使能信号、操作码这类端口通常位宽较窄取值空间有限。例如一个3位模式选择信号mode[2:0]其合法值可能只有3b000到3b100这5种。对于这类控制敏感型转换其测试空间虽然可能包含多个信号的组合但总数通常可控几十到几百。我们的策略是在ATPG的多轮遍历中对该转换进行多次触发每次尝试覆盖其测试空间中的一个独特组合。目标是尽可能逼近穷举覆盖确保所有控制模式都被验证到。3.2.2 数据敏感型转换的智能采样覆盖如果一个转换的条件函数涉及数据路径端口如待处理的数据、地址、计算操作数这类端口位宽通常较宽如32位、64位其理论取值空间是天文数字。对于这类数据敏感型转换穷举覆盖既无必要也不可能。数据端口的值大部分是“等效”的关键在于覆盖边界值和特殊值。我们的测试空间覆盖策略会识别数据敏感型转换并采用基于边界值分析和等价类划分的智能采边界值对于比较操作如in1 65536重点生成in1 65535边界内最大值、in1 65536边界值通常应不满足条件、in1 0、in1 -1如果是有符号数等。特殊值生成全0、全1、交替01等容易暴露数据通路缺陷的模式。与变量相关的约束如果条件涉及变量如data register则策略会与回跳算法协同在设置该register值时就为其选择有代表性的数据从而间接为数据端口生成有意义的测试值。通过结合转换遍历引擎保证广度和测试空间覆盖策略追求深度我们的ATPG方法能够为STG模型生成一套高效且高覆盖率的测试向量集这些向量不仅走通了所有功能路径还在每条路径上尝试了最有可能会引发问题的输入组合。注意事项测试空间划分的实践区分“控制敏感”和“数据敏感”并非总是泾渭分明。在实践中需要根据设计规范来判断端口的首要功能。一个常见的技巧是查看该端口在规范中是被描述为决定“做什么”控制还是决定“对什么数据做”数据。也可以根据位宽和经验初步判断再通过初始的随机测试观察其取值对覆盖率的影响来调整。将本应是数据端口的信号误判为控制端口并试图穷举会导致测试用例爆炸反之则可能遗漏重要的控制状态。4. 从方法到工具STG-Test的实现与应用理论方法最终需要工程化工具来落地。我们开发了一款名为STG-Test的自动硬件/软件协同验证工具实现了上述基于STG的半形式化验证流程。STG-Test的设计遵循用户友好和自动化两个核心原则。4.1 图形化建模界面为了让验证工程师能够直观、便捷地从设计规范创建STG模型STG-Test提供了一个专门的图形用户界面。用户无需手动编写复杂的模型描述文件而是通过GUI进行拖拽和配置定义端口和变量在界面中声明设计的输入输出端口位宽、类型以及规范中提到的内部变量及其初始值。绘制阶段与转换通过画布工具创建阶段节点并用有向边连接它们以表示转换。配置转换属性点击每条转换在弹出的属性窗口中以类C语言的表达式或脚本形式定义其条件函数βt、反应函数αt和时序标记Ct。GUI会提供语法高亮和基础检查。模型检查与可视化工具内置模型检查器可以检测STG中的死锁、不可达阶段、条件冲突等问题并以高亮方式提示用户。图形化的呈现方式使得复杂的时序逻辑关系一目了然。这个GUI将形式化建模的门槛大大降低使得系统工程师甚至软件工程师也能参与到前期的功能模型构建中促进了设计团队与验证团队的早期协作。4.2 自动化验证流程一旦STG模型建立STG-Test便可以连接主流的RTL仿真器如VCS, ModelSim, Verilator等启动全自动的验证流程测试生成与驱动STG-Test内部的ATPG引擎根据前述策略动态生成测试向量。这些向量通过工具生成的测试平台Testbench自动施加到被测设计DUV的输入端口。响应监控与检查测试平台同时监控DUV的输出和内部变量对应STG中的V。在每一个时钟周期工具都会根据当前STG所处的阶段、激活的转换以及时序标记Ct来预测DUV应有的输出行为和变量变化。自动断言与错误报告如果DUV的输出或变量值在预期的周期内与STG模型的预测不符工具会立即报告一个功能错误或时序违例并详细记录出错时的仿真时间、阶段、转换、预期值与实际值。这种检查是内嵌在仿真过程中的动态断言比事后查看波形图要高效、准确得多。覆盖率收集与反馈验证结束后工具自动生成两份覆盖率报告基于STG的功能覆盖率报告每个STG、每个阶段、每条转换的触发次数以及每个转换的测试空间覆盖百分比对控制敏感型转换尤其有用。这直接衡量了规范被验证的完备程度。代码覆盖率通过仿真器接口收集DUV的代码行覆盖率、条件覆盖率、分支覆盖率等。这衡量了实现被测试的充分程度。4.3 实验评估与效果分析我们在多个基准测试电路如ITC99基准集和内部真实的硬件设计模块上评估了STG-Test。与传统的基于实现的半形式化方法如从RTL提取EFSM模型进行对比结果显示验证效率在达到相似代码覆盖率如95%以上的行覆盖的前提下基于STG的方法所需的测试向量数量和仿真时间通常更少。这是因为STG模型直接针对功能点生成测试避免了从实现中提取模型可能引入的冗余和无关状态。错误发现能力我们向一些设计中注入了已知的功能错误如遗漏条件分支、时序计算错误、边界条件处理不当。STG-Test能够有效地触发这些错误特别是那些与规范中明确描述的多周期时序或复杂条件组合相关的错误。可扩展性与实用性对于控制逻辑复杂的状态机如仲裁器、协议控制器和数据通路复杂的计算单元如滤波器、加密模块STG模型都能很好地描述其行为。由于模型源于规范在RTL代码尚未稳定或频繁更改的早期阶段验证工作就可以同步开展实现了“左移”。5. 常见挑战与工程实践心得尽管基于STG的方法优势明显但在实际工程应用中我们仍会遇到一些挑战并积累了一些宝贵的经验。5.1 挑战一规范歧义与不完整性设计规范可能存在歧义、二义性或遗漏。STG建模过程本身就是一个对规范的深度审查过程。应对策略在建模时一旦发现模糊之处必须立即与设计作者或系统架构师澄清并将澄清后的结论作为注解记录在STG模型中。这不仅能完善模型也促进了团队对需求的共同理解避免了后期的返工。5.2 挑战二复杂数据操作的建模规范中可能包含复杂的数学运算、非线性函数或动态数据结构。在STG的反应函数αt中精确描述这些操作可能很困难。应对策略STG-Test支持调用外部函数或引用预定义的运算库。对于非常复杂的数据操作可以在反应函数中将其抽象为一个函数调用如[out complex_math_func(in1, in2)]然后在测试平台中实现该函数的参考模型。验证的重点在于控制流和时序数据路径的正确性可以通过对比DUV输出与参考模型输出在满足时序的前提下来保证。5.3 挑战三并发与交互功能的建模一个设计通常包含多个并发运行的功能点。如何用多个STG来描述它们之间的交互应对策略为每个主要功能点建立独立的STG。对于功能点间的交互如握手、仲裁、数据共享可以通过共享变量或定义全局事件来建模。例如功能点A完成后将一个共享标志变量置位功能点B的条件函数可以检查这个变量。STG-Test的调度器会管理多个STG的并发执行和变量同步。关键在于交互的语义必须在规范中有明确定义。5.4 实操心得模型调试与迭代STG模型本身也可能有“bug”。一个常见的现象是ATPG过程卡住无法覆盖某些转换。排查流程检查控制依赖首先确认回跳算法是否正确地分析了变量依赖关系。工具应能可视化展示控制依赖图。审查条件函数仔细检查未覆盖换的条件函数βt是否逻辑上可能为真是否存在矛盾例如(a5) (a3)检查时序标记确认时序标记Ct是否合理一个过小的Ct可能导致DUV在预期周期内无法完成操作从而永远等不到预期的输出导致转换无法“完成”。仿真调试让工具在尝试触发该转换时输出更详细的调试信息包括每个周期各个变量的值、尝试满足的约束条件等。结合波形图观察DUV的实际行为。迭代建模功能验证是一个迭代过程。初始的STG模型可能比较粗糙。随着验证的进行根据代码覆盖率和发现的错误可能需要回头补充或修正STG模型例如增加之前忽略的异常处理分支或修正某个时序。应将STG模型视为与设计文档同等重要的、需要持续维护的活文档。5.5 性能优化技巧对于大型设计STG模型可能变得复杂ATPG和仿真时间会增长。分层验证先为底层子模块建立STG并单独验证再为集成后的系统级功能建立更高层次的STG。底层STG可以被复用为高层STG的“抽象动作”。合理剪枝对于某些在特定模式下才使能的功能可以在STG中通过条件判断提前排除无关的转换遍历减少搜索空间。并行执行STG-Test支持将不同的STG或同一STG的不同初始条件生成的测试用例分配到不同的仿真进程或机器上并行执行以缩短总体验证时间。基于STG的半形式化验证方法将验证的焦点从代码实现拉回到了功能规范本身通过一种直观的图形化模型和系统化的测试生成策略在形式化的严谨性与仿真的灵活性之间找到了一个高效的平衡点。它不仅是发现bug的工具更是促进团队对设计需求达成一致理解、实现“第一次就做对”理念的重要桥梁。