北大团队提出神经符号智能体框架，RTL 自动修复率达 96.8%，平均单次修复成功率 87.5%

一块芯片从设计到流片，验证和调试要吃掉大半研发周期。硬件工程师的日常是这样的：写好测试平台，跑仿真，盯着成百上千条信号波形，找那一个跳变不对的时钟周期，顺藤摸瓜定位到代码，改一行，再跑一遍。如此循环几十次，一个 bug 才算修完。遇到复杂系统，这个试错循环可能反复几十轮，每一轮都是实打实的人力和机器时间。

北京大学的研究团队最近公布了 Clover 框架，想把这个循环交给大模型智能体自动完成。在业界广泛使用的 RTL-Repair 基准上，Clover 在限定时间内修好了 96.8% 的 bug，平均单次修复成功率达到 87.5%。更关键的是，整个过程不依赖人工撰写的设计说明书，智能体能看到的只有源代码和顶层模块的输入输出波形，设定上和传统自动修复方法一样苛刻。

RTL 调试这笔账，为什么这么贵

寄存器传输级代码，也就是工程师口中的 RTL，是芯片设计的主战场。设计意图先用 RTL 写下来，再综合成网表，最后经仿真产生波形。调试的任务，是在发现功能错误后用尽量小的代码改动恢复正确性。

典型的手工调试分三步。先构造能暴露 bug 的测试用例，再分析波形或断言把嫌疑范围缩小到某段代码，最后动手打补丁，同时尽量控制改动范围。听起来清晰，做起来全是反复。波形里信号动辄几百条，错误的表现和错误的根源之间可能隔着好几个模块，工程师只能靠经验猜一个可能的原因，改了再说，不对就换下一个猜测。每一轮猜测都伴随着一次完整的仿真和检查，复杂系统里这个循环可以耗掉数周。

论文讨论的自动修复聚焦在后两步，即假设 bug 已经被测试暴露，剩下的事是定位并修掉它。正确性的判据也很工程化：打补丁后的仿真波形要和黄金参考波形逐拍对齐。这个判据既是大模型容易理解的接口，也是 RTL 调试领域的通行标准。

自动程序修复，英文简称 APR，想把后两步自动化。这条路上有两类玩家。

第一类是传统符号方法，代表作有 CirFix、RTL-Repair 和 Strider。它们的思路是把修复变成一个可求解的问题：预先定义一批修复模板，比如替换某个常量、给信号加一个守卫条件，然后用程序综合或 SMT 求解器在模板划定的解空间里搜索。SMT 求解器是一种自动定理证明工具，擅长在严格约束下求出精确解。这类方法的优点是答案严格、可验证，缺点也同样明显：模板之外的 bug 一概修不了。

第二类是这几年兴起的大模型方法。大模型读过海量 RTL 代码和自然语言文档，可以直接在词元空间里生成补丁，不受模板限制。但它有两个老毛病。一是随机性，同样的输入跑几次，结果可能天差地别。二是上下文脆弱，RTL 代码本来就长，再塞进密集的波形数据，模型的注意力很快被淹没，开始分心、幻觉，给出看着像样实则离谱的改动。

两条路线各有死穴，这正是 Clover 要破的局。

一张光谱图说清：RTL 修复没有银弹

Clover 论文里有一张很能说明问题的图，把常见的修复操作排成了一条光谱。

图 1：RTL 修复操作光谱。高抽象层的修复操作更适合大模型，低抽象层的更适合符号方法，算法级错误目前任何自动方法都难以处理。

图片来源：原论文 Figure 1。

光谱的纵轴是抽象层次，从上往下依次是设计意图、RTL 源码、网表、波形，正好对应芯片设计的自然流程。横轴是识别出正确修复操作的难度。

排在高层的操作，比如按照自然语言规格对齐行为、调整编码风格、增删子模块，本质上是对设计意图的理解和重组，恰好是大模型的主场。排在低层的操作，比如改一个字面量常数、重写布尔表达式、把信号提前或推后一个时钟周期，涉及的是网表和波形级别的精确数值关系，更适合符号求解器一步步推出来。光谱的最右端是算法级错误，比如整个状态机的设计思路就错了，这类问题超出了现有所有自动修复方法的能力边界。

论文把这条光谱细分为十二类典型操作，值得逐一看一眼。最贴近设计意图的是按规格对齐行为，需要读懂自然语言描述。往下是编码风格，比如把敏感列表统一改成时钟上升沿，以及增删信号依赖、实例化或移除子模块。语法错误和握手接口问题处于中高层，模式固定，大模型见得多了自然手熟。控制流错误，比如 if-else 分支或 generate 循环写错，开始牵涉具体数值行为。再往下是周期移位，要通过插入或移除流水线寄存器把信号在时间上对齐。最底层是字级表达式、布尔表达式和字面量，改的全是比特级的精确取值。越往低层走，修复动作越微观，但对错越没有含糊的余地。

真正棘手的地方在于，一个实际的修复往往需要多种操作配合。论文把这种现象称为多步异构性。比如先用大模型给信号补一条依赖，再让求解器把布尔表达式调对，两步操作性质完全不同，缺了哪一步都修不好。而规格说明又只存在于光谱的两个极端：高层有自然语言描述的设计意图，低层有波形断言构成的精确约束，中间层什么都没有。符号方法从低层原语出发构造搜索空间，抽象层次每上升一层，空间就指数膨胀一次，很快就退化成了靠手工启发式规则引导的非严格搜索。大模型从高层信息出发，一遇到低层的密集波形就上下文爆炸。任何单一技术路线都覆盖不了整条光谱，这就是论文的核心判断。

已有方法的能力边界

论文把主流方法按故障定位手段、补丁生成手段和修复能力做了一张对照表，格局一目了然。

图 2：主流 RTL 自动修复方法的能力对比。

图片来源：原论文 Table 1。

传统方法里，CirFix 和 RTL-Repair 干脆不做故障定位，直接在可疑范围内套模板；Strider 靠信号追踪定位，功能强但依赖内部信号波形，实际中经常拿不到。大模型方法里，RTLFixer 主要修语法错误，UVLLM 结合了 linter 检查和信号追踪，能力算中等，但仍要求输入一段问题描述文本。修复能力这一项，传统方法清一色受限于模板，大模型方法徘徊在弱到中等。

Clover 在表格里的那一行很有意思：故障定位靠分析加经验，补丁生成同时动用经验、试错和求解三种手段，修复能力标注为强。它不是在某一个环节上做文章，而是把整条流水线重新组织了一遍。

Clover 的总体设计：一个会提假设的主智能体

Clover 的全称里有两个关键词，神经符号和智能体框架。神经指大模型，符号指 SMT 求解器，智能体框架则是把两者组织起来的脚手架。整个系统的总指挥是主智能体，它的工作流是一个三层嵌套循环，模拟的正是人类工程师的调试心智。

图 3：Clover 框架总览，包含主智能体、上下文智能体、SMT 符号修复和假设树四个部分。

图片来源：原论文 Figure 2。

最外层是假设环。工程师面对 bug 会先猜一个根因，验证，猜错了再换。主智能体也一样，它会主动提出新假设，或者在一个假设上消耗的操作预算超标时触发耐心耗尽机制，强制换方向。这个设计很务实，防止系统在一条死路上把时间和算力烧光。

中间层是验证环。拿到一个假设后，主智能体先让上下文智能体取回相关代码，看 linter 有没有报错，有就叫 lint 修复智能体处理，然后进入补丁环。每一轮验证只应用一个补丁，补丁逐轮累积，多步修复由此成为可能。

最内层是补丁环。主智能体在这里收集构造补丁所需的一切信息，可以看代码片段，可以看波形文件，也可以向上下文智能体追问。信息够了，它要么直接写出补丁，要么判断当前 bug 适合某个符号修复模板，把活儿派给 SMT 求解器。

创新一：分工明确的多智能体与 RTL 专用工具箱

主智能体手底下有两个专职下属，分工的逻辑是保护主对话的上下文干净。

上下文智能体负责从庞大的 RTL 代码库里取出关键代码片段。主智能体每提出一个假设，就新建一个上下文智能体实例，这个实例在该假设的整个验证周期里维持连续对话。它背后接入了 slang-server 语言服务器，就是 VS Code 这类编辑器背后做代码导航的那套基础设施，可以查符号定义、查所有引用位置，沿着信号依赖和模块层级在代码库里游走，最后把浓缩后的结论返回给主智能体。

lint 修复智能体处理的是另一类琐碎但高频的任务。Verilator 报的错误和警告，由它接手分析并给出修复或忽略的决定。论文把它单独拆出来的理由很直白：lint 问题对大模型来说不难，但数量实在太多，全堆在主对话里会严重污染上下文。

工具箱里的几件家当也值得一看。VCD 查看器把波形文件转成指定时间窗内的文本信号轨迹，自动高亮和黄金参考波形有偏差的位置，还会抑制宽位总线信号防止刷屏。自定义 linter 构建在 Yosys 处理过的网表之上，专门抓那些符合 Verilog 语法但工程上极易出错的写法，比如一个信号被多处驱动、一根线只有部分位被驱动。仿真器则可以直接调用，反馈即时回到智能体手里。

这套设计的取向很清楚：不让大模型干它不擅长的脏活累活，把信息过滤、代码导航、波形提取这些环节全部工具化，大模型只做判断和决策。

创新二：把 SMT 求解器从后台流水线变成智能体的工具

符号修复这一翼，Clover 站在 RTL-Repair 的肩膀上，但做了三处关键改造。

先回顾基本原理。RTL-Repair 把硬件设计综合成有界模型检测下的转移模型，把波形规格写成输入输出上的断言，再把修复选项编码成自由变量，整个问题丢给 SMT 求解器。求解器给出答案，修复就有着落了。原始版本提供三个模板，分别对应换字面量、加守卫条件和条件覆写。

第一处改造是新增周期移位模板，专门对付跨时钟周期的时序 bug。一个信号到底是组合逻辑直连还是经过一级寄存器，决定了它和上游信号同拍变化还是晚一拍。Clover 的建模方式很巧妙：在信号路径上插一个多选器，一路直连，一路过寄存器，多选器的选择信号是一个自由变量，交给求解器去定。往所有信号上无差别地插多选器会引入组合环，纯符号方法根本不敢这么做，因为求解器不知道该改哪些信号。但在 Clover 里，主智能体已经通过波形分析锁定了嫌疑信号，模板只落在该落的地方。这个模板在纯符号流程里不可行，在智能体引导下反而安全，是神经符号互补的一个漂亮注脚。

图 4：周期移位 bug 的建模方式，自由变量的取值由 SMT 求解器决定。

图片来源：原论文 Figure 3。

第二处改造在流程上。原来的 RTL-Repair 是把三个模板按固定顺序挨个试，撞上一个算一个。Clover 把模板选择权交给主智能体，并详细告知每个模板的效果和适用条件。模板选择从一个机械的后台步骤，变成了由调试上下文指导的主动决策。

第三处改造在结果回写。求解器不再直接改源码，而是返回结构化的修复动作，比如某处表达式重写、某处插入守卫。主智能体再根据这些动作生成最终的源码级补丁，尽量沿用原有的控制流结构、语句顺序和编码风格。举个例子，要改某个信号的条件，智能体会找一个合适的 if-else 分支下手，而不是生硬地塞进一棵多选器树。论文还顺手把这套流程从 Verilog 扩展到了 SystemVerilog，覆盖面更广。

创新三：随机思维树，把大模型的坏毛病变成搜索资源

大模型的随机性通常被视为灾难，Clover 的第三个创新偏要反着来：既然每次生成本来就有随机性，不如把它组织成一场可控的搜索。

思维树是一种测试时扩展技术，把大模型的推理组织成搜索树，在推理时投入更多算力换取更好的结果。Clover 让主智能体提出的假设在树上生长：每个节点可以分出多个子节点，对应基于父节点验证过程中观察到的新信息而提出的新假设。修复过程中，代码状态和对话历史被完整记录在节点里，随时可以回滚到任何一个节点继续探索。

原版思维树有两个问题。它用深度优先或广度优先加束搜索来遍历，并且让大模型自己评估每个节点的价值。让模型给自己的中间状态打分，结果可想而知，搜索近乎盲目。

Clover 换成了随机采样加启发式打分。启发式函数不看模型脸色，只看五个可客观统计的量：已通过的测试平台数量、从设计中查询到的信息量、未解决的编译错误数、已消耗的 token 数、已应用的补丁数，外加一个调节探索倾向的基值。通过测试越多、获取信息越多，节点得分越高；编译错误越多、补丁和 token 消耗越大，得分越低。这些量都能在验证循环里顺手统计，不需要任何模型参与评估。

打分之后的节点选择环节，论文没有用贪心的最高分优先，而是按 softmax 分布采样。每个节点的得分先取指数，再除以所有节点指数得分的总和，得到的概率值决定它被选中的机会。指数运算放大了得分差距，好节点大概率被优先展开；采样的随机性又给暂时落后的节点留了机会，搜索不会在局部最优里困死。选中之后，系统恢复该节点保存的代码状态和对话历史，主智能体接着跑，直到提出新假设，新节点入树，进入下一轮采样。

这就是探索与利用的平衡。论文给出的系数配置里，通过测试的权重是 50，编译错误的惩罚权重是 5，token 的惩罚权重只有 0.0005，量级差异背后是设计者的取舍：修好是第一位的，省钱是次要的。而且作为测试时扩展手段，这些系数随时可调，不需要重新训练任何模型。

实验：32 个 bug 修好 31 个

看疗效。评测用的是 RTL-Repair 基准，32 个带 bug 的 RTL 设计，bug 根源从结构性错误到算法性错误都有，这个基准被此前多篇工作采用。判定标准很严格：打补丁后的仿真波形必须和黄金参考完全一致。基线选了三个代表，传统方法的标杆 RTL-Repair，以及两个开源的大模型方法 MEIC 和 UVLLM。

实验设定刻意压低了人工辅助：没有自然语言设计说明，大模型只能看到源代码和顶层模块的输入输出波形。底层模型走的是 Seed2code 的 API。为了量化可靠性，论文采用 pass@k 指标，即 k 次独立重试内修复成功的概率，每个案例跑 10 次重试，每次限时 30 分钟、总 token 上限 200 万。基线方法不支持这种限制，论文调整了它们的轮数和重试次数，让时间开销大致相当。

图 5：RTL-Repair、MEIC、UVLLM 与 Clover 的修复能力对比，Clover 修复 31 个，基线分别为 16、10、19 个。

图片来源：原论文 Figure 4。

结果相当悬殊。Clover 修好 31 个，RTL-Repair、MEIC、UVLLM 分别修好 16 个、10 个和 19 个。换算成相对数字，Clover 比传统方法多修了 94% 的 bug，比大模型方法多修了 63%。平均 pass@1 达到 87.5%，意味着大多数案例一次就能修成。开销方面，平均每个案例用时 413.8 秒，排除失败案例后只有 241.8 秒，平均 token 消耗约 29.5 万。

前 17 个基准是单模块单文件的简单案例，大模型轻松拿下，但过程并非全无波澜。论文提到一个细节：基准里的 3-to-8 译码器带一个没什么用处的使能信号，和教科书里的常见写法不一样，智能体一开始被这个反常设计绕晕了，靠着试错验证自己的理解才回过神来。这恰好说明假设验证循环的价值，第一印象错了没关系，仿真反馈会纠偏。

真正的分水岭在后 15 个复杂案例，bug 的根因深埋在模块树和文件结构里。论文的分析里有不少生动的细节。sha3_r1、pairing_k1、reed_b1 是信号或表达式宽度写错，Verilator 的警告能撞上。sha3_w1 有一根线部分位没被驱动，pairing_w2 把模块的输入输出接反了，语法都合法，靠自定义 linter 才现形。pairing_w1 是个死循环，循环变量方向写反，属于算法级错误，行为可疑所以被智能体盯上。最难的是 sha3_w2 和 sha3_s1，前者把条件误写成 0 还把线网错当成寄存器，后者在缓冲区满时丢了一个更新条件，都叠加了多种修复操作，靠假设树搜索才找到解。

唯一的失手是 i2c_k1。i2c 系列基准需要模拟周期内延迟和高阻态，属于另一类 RTL 设计，现有工具链支持得不好。论文对此没有回避，直接写明了失败原因。

基线的问题也被逐一拆解。RTL-Repair 的模板覆盖不了 decoder_w2、fsm_w1 这类控制结构错误；它虽然通过了 i2c_k1，但靠的是人工把修复范围指定到 bug 所在文件来压缩求解规模，这在最小人工引导的设定下属于违规操作。MEIC 用一个打分智能体给 RTL 代码排序，进一步放大了不稳定性。UVLLM 需要一段问题描述文本作为输入，设定里没有这份文本，给了描述也只能多过 counter 的简单案例。counter 案例暴露了信号追踪的短板：追踪穿不透组合逻辑，而设计里溢出信号和使能信号又没有关联，靠经验打补丁同样失效。没有规格说明时，大模型容易幻觉上头，把整个设计推倒重写，Clover 靠假设验证和反馈审查挡住了这种危险。论文还提到一个公平性细节，基准中 reed_o1 的原始测试平台本身无效，作者保持原样不做修复，只为和此前工作公平对比。

消融实验与合成基准：两个创新都有贡献

光看总分不够，论文还做了消融实验，把随机思维树和 SMT 修复分别关掉，在 15 个复杂基准上对比。

图 6：消融实验，完整配置的 pass@1 最高，时间和 token 开销的上升在可接受范围内。

图片来源：原论文 Figure 5。

结论清晰。关掉思维树，主智能体只能在上一个假设的基础上线性迭代，pass@1 垫底，论文解释说复杂 bug 需要探索多样化的根因假设，线性链条经常走进死胡同。关掉 SMT，pass@1 同样落后于完整配置，符号修复在特定案例上起到了稳定军心的作用。完整配置在三个指标上都是最高，时间和 token 随之上浮，但幅度温和，成功试次平均 241 秒，比起 1800 秒的超时上限还有很大余量。论文也坦承提升幅度不算大，原因之一是所选基准还不够难，基线 pass 率本就超过 75%。

另一个质疑同样需要回应：RTL-Repair 基准都是常见硬件模块，网上有开源实现，说不定早就在大模型的训练语料里躺过了。为此论文构造了八个合成基准，纯随机逻辑，随机连线的信号和运算符，没有任何语义和实用价值，确保不可能出现在训练数据里，再往里注入各种 bug。这一轮关闭了 SMT 修复，纯考智能体的分析能力。

结果八个全部修复，六个达到 100% 的 pass@1，剩下两个也有 80%。那两个 80% 的案例要求智能体在几乎无上下文的情况下猜出正确运算符，本质上是程序合成任务，成功率低在情理之中。组合逻辑错误的几例，比如表达式里多了一项、少了一项、条件被取反，都能从波形轨迹里推断出来，展示了智能体做简单逻辑推理的能力。表达式缺项的那一例更难，因为要引入新的信号依赖，需要更多轮猜测。信号延迟或提前一拍的两类时序 bug，智能体靠着波形转储功能观察到信号在轨迹里的拍差，也都修好了。这说明 Clover 的能力不是背答案，而是真的能面对全新设计做调试。

这项工作留下的启示

Clover 的意义不止于一个修复率的数字。

对 EDA 领域来说，它示范了智能体框架工程的完整打法。工具链适配、上下文工程、领域技能、子智能体分工，这些在软件智能体里被反复验证的手段，系统性搬进硬件调试场景后同样奏效。大模型不需要重新训练，套上合适的脚手架就能扛起专业任务。

对智能体研究来说，随机思维树提供了一种驯服随机性的新视角。与其把采样噪声当作需要消除的误差，不如把它当作搜索的燃料，用可客观统计的启发式信号引导方向，用概率采样保留多样性。整个机制不需要训练，调几个系数就能改变搜索性格。

对神经符号这个老命题，Clover 给出了一个干脆的分工原则：让大模型做高层编排，把低层的精确调整交给符号求解器。符号方法的刚性，要么严格满足规格要么彻底失败，决定了它不适合当主角，但当工具正合适。

局限也摆在那里。需要周期内时序语义的设计还修不了，算法级错误依旧无解，求解器和 API 调用的成本在大规模部署时也得算账。论文没有吹嘘这些问题的解决，只是如实标注了边界。

结语

RTL 自动修复的难，难在没有任何单一技术能覆盖从高抽象意图到低抽象波形的整条修复光谱。Clover 的思路是把这场修复组织成一次结构化的搜索：主智能体像工程师一样提出假设、验证假设，把低层精确修复外包给 SMT 求解器，再用随机思维树把大模型与生俱来的随机性转化成探索的动力。

96.8% 的修复率和 87.5% 的平均 pass@1，说明这条路走得通。当大模型的每一次试错都被记录、打分、采样，运气就变成了策略。硬件调试这个最依赖老师傅经验的环节，正在迎来一套可复制、可调参、可扩展的自动化方案。

参考资料

图片来源说明：本文部分图片改编自原论文，仅用于论文解读与学术交流。