北大团队提出神经符号智能体框架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 论文里有一张很能说明问题的图把常见的修复操作排成了一条光谱。图 1RTL 修复操作光谱。高抽象层的修复操作更适合大模型低抽象层的更适合符号方法算法级错误目前任何自动方法都难以处理。图片来源原论文 Figure 1。光谱的纵轴是抽象层次从上往下依次是设计意图、RTL 源码、网表、波形正好对应芯片设计的自然流程。横轴是识别出正确修复操作的难度。排在高层的操作比如按照自然语言规格对齐行为、调整编码风格、增删子模块本质上是对设计意图的理解和重组恰好是大模型的主场。排在低层的操作比如改一个字面量常数、重写布尔表达式、把信号提前或推后一个时钟周期涉及的是网表和波形级别的精确数值关系更适合符号求解器一步步推出来。光谱的最右端是算法级错误比如整个状态机的设计思路就错了这类问题超出了现有所有自动修复方法的能力边界。论文把这条光谱细分为十二类典型操作值得逐一看一眼。最贴近设计意图的是按规格对齐行为需要读懂自然语言描述。往下是编码风格比如把敏感列表统一改成时钟上升沿以及增删信号依赖、实例化或移除子模块。语法错误和握手接口问题处于中高层模式固定大模型见得多了自然手熟。控制流错误比如 if-else 分支或 generate 循环写错开始牵涉具体数值行为。再往下是周期移位要通过插入或移除流水线寄存器把信号在时间上对齐。最底层是字级表达式、布尔表达式和字面量改的全是比特级的精确取值。越往低层走修复动作越微观但对错越没有含糊的余地。真正棘手的地方在于一个实际的修复往往需要多种操作配合。论文把这种现象称为多步异构性。比如先用大模型给信号补一条依赖再让求解器把布尔表达式调对两步操作性质完全不同缺了哪一步都修不好。而规格说明又只存在于光谱的两个极端高层有自然语言描述的设计意图低层有波形断言构成的精确约束中间层什么都没有。符号方法从低层原语出发构造搜索空间抽象层次每上升一层空间就指数膨胀一次很快就退化成了靠手工启发式规则引导的非严格搜索。大模型从高层信息出发一遇到低层的密集波形就上下文爆炸。任何单一技术路线都覆盖不了整条光谱这就是论文的核心判断。已有方法的能力边界论文把主流方法按故障定位手段、补丁生成手段和修复能力做了一张对照表格局一目了然。图 2主流 RTL 自动修复方法的能力对比。图片来源原论文 Table 1。传统方法里CirFix 和 RTL-Repair 干脆不做故障定位直接在可疑范围内套模板Strider 靠信号追踪定位功能强但依赖内部信号波形实际中经常拿不到。大模型方法里RTLFixer 主要修语法错误UVLLM 结合了 linter 检查和信号追踪能力算中等但仍要求输入一段问题描述文本。修复能力这一项传统方法清一色受限于模板大模型方法徘徊在弱到中等。Clover 在表格里的那一行很有意思故障定位靠分析加经验补丁生成同时动用经验、试错和求解三种手段修复能力标注为强。它不是在某一个环节上做文章而是把整条流水线重新组织了一遍。Clover 的总体设计一个会提假设的主智能体Clover 的全称里有两个关键词神经符号和智能体框架。神经指大模型符号指 SMT 求解器智能体框架则是把两者组织起来的脚手架。整个系统的总指挥是主智能体它的工作流是一个三层嵌套循环模拟的正是人类工程师的调试心智。图 3Clover 框架总览包含主智能体、上下文智能体、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编译错误的惩罚权重是 5token 的惩罚权重只有 0.0005量级差异背后是设计者的取舍修好是第一位的省钱是次要的。而且作为测试时扩展手段这些系数随时可调不需要重新训练任何模型。实验32 个 bug 修好 31 个看疗效。评测用的是 RTL-Repair 基准32 个带 bug 的 RTL 设计bug 根源从结构性错误到算法性错误都有这个基准被此前多篇工作采用。判定标准很严格打补丁后的仿真波形必须和黄金参考完全一致。基线选了三个代表传统方法的标杆 RTL-Repair以及两个开源的大模型方法 MEIC 和 UVLLM。实验设定刻意压低了人工辅助没有自然语言设计说明大模型只能看到源代码和顶层模块的输入输出波形。底层模型走的是 Seed2code 的 API。为了量化可靠性论文采用 passk 指标即 k 次独立重试内修复成功的概率每个案例跑 10 次重试每次限时 30 分钟、总 token 上限 200 万。基线方法不支持这种限制论文调整了它们的轮数和重试次数让时间开销大致相当。图 5RTL-Repair、MEIC、UVLLM 与 Clover 的修复能力对比Clover 修复 31 个基线分别为 16、10、19 个。图片来源原论文 Figure 4。结果相当悬殊。Clover 修好 31 个RTL-Repair、MEIC、UVLLM 分别修好 16 个、10 个和 19 个。换算成相对数字Clover 比传统方法多修了 94% 的 bug比大模型方法多修了 63%。平均 pass1 达到 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消融实验完整配置的 pass1 最高时间和 token 开销的上升在可接受范围内。图片来源原论文 Figure 5。结论清晰。关掉思维树主智能体只能在上一个假设的基础上线性迭代pass1 垫底论文解释说复杂 bug 需要探索多样化的根因假设线性链条经常走进死胡同。关掉 SMTpass1 同样落后于完整配置符号修复在特定案例上起到了稳定军心的作用。完整配置在三个指标上都是最高时间和 token 随之上浮但幅度温和成功试次平均 241 秒比起 1800 秒的超时上限还有很大余量。论文也坦承提升幅度不算大原因之一是所选基准还不够难基线 pass 率本就超过 75%。另一个质疑同样需要回应RTL-Repair 基准都是常见硬件模块网上有开源实现说不定早就在大模型的训练语料里躺过了。为此论文构造了八个合成基准纯随机逻辑随机连线的信号和运算符没有任何语义和实用价值确保不可能出现在训练数据里再往里注入各种 bug。这一轮关闭了 SMT 修复纯考智能体的分析能力。结果八个全部修复六个达到 100% 的 pass1剩下两个也有 80%。那两个 80% 的案例要求智能体在几乎无上下文的情况下猜出正确运算符本质上是程序合成任务成功率低在情理之中。组合逻辑错误的几例比如表达式里多了一项、少了一项、条件被取反都能从波形轨迹里推断出来展示了智能体做简单逻辑推理的能力。表达式缺项的那一例更难因为要引入新的信号依赖需要更多轮猜测。信号延迟或提前一拍的两类时序 bug智能体靠着波形转储功能观察到信号在轨迹里的拍差也都修好了。这说明 Clover 的能力不是背答案而是真的能面对全新设计做调试。这项工作留下的启示Clover 的意义不止于一个修复率的数字。对 EDA 领域来说它示范了智能体框架工程的完整打法。工具链适配、上下文工程、领域技能、子智能体分工这些在软件智能体里被反复验证的手段系统性搬进硬件调试场景后同样奏效。大模型不需要重新训练套上合适的脚手架就能扛起专业任务。对智能体研究来说随机思维树提供了一种驯服随机性的新视角。与其把采样噪声当作需要消除的误差不如把它当作搜索的燃料用可客观统计的启发式信号引导方向用概率采样保留多样性。整个机制不需要训练调几个系数就能改变搜索性格。对神经符号这个老命题Clover 给出了一个干脆的分工原则让大模型做高层编排把低层的精确调整交给符号求解器。符号方法的刚性要么严格满足规格要么彻底失败决定了它不适合当主角但当工具正合适。局限也摆在那里。需要周期内时序语义的设计还修不了算法级错误依旧无解求解器和 API 调用的成本在大规模部署时也得算账。论文没有吹嘘这些问题的解决只是如实标注了边界。结语RTL 自动修复的难难在没有任何单一技术能覆盖从高抽象意图到低抽象波形的整条修复光谱。Clover 的思路是把这场修复组织成一次结构化的搜索主智能体像工程师一样提出假设、验证假设把低层精确修复外包给 SMT 求解器再用随机思维树把大模型与生俱来的随机性转化成探索的动力。96.8% 的修复率和 87.5% 的平均 pass1说明这条路走得通。当大模型的每一次试错都被记录、打分、采样运气就变成了策略。硬件调试这个最依赖老师傅经验的环节正在迎来一套可复制、可调参、可扩展的自动化方案。参考资料图片来源说明本文部分图片改编自原论文仅用于论文解读与学术交流。