④ RTL-Repair: Fast Symbolic Repair of Hardware Design Code

可译为：

《RTL-Repair：硬件设计代码的快速符号化修复》

更详细的翻译：

《RTL-Repair：一种面向硬件设计代码的快速符号推理修复方法》

词语拆解：

• Fast
  快速的
• Symbolic Repair
  符号化修复 / 基于符号方法的修复
  这里的 symbolic 往往指形式化方法中的符号执行、符号推理、约束求解等，而不是靠神经网络直接生成。
• Hardware Design Code
  硬件设计代码

整体理解：

这篇标题的重点是：
使用符号方法、形式化推理或约束求解来快速修复 RTL / 硬件设计代码。
和依赖 LLM 的方法相比，这类方法通常更强调可验证性、严谨性、正确性保证。（不是LLM的方法这意思）（传统的方法，还有点复杂）

这篇论文研究的是：能不能自动帮硬件工程师修 RTL（寄存器传输级）代码里的 bug，而且要修得又快又靠谱。 作者提出了一个工具叫 RTL-Repair，目标是根据“有 bug 的 Verilog 代码 + 测试信息”，自动生成一个修改建议，让电路重新通过测试。

一、这篇论文在讲什么

作者的核心判断是：硬件设计里的很多逻辑 bug 都发生在 RTL 层，而传统调试方式很依赖工程师手工看波形、推断错误位置，这件事很费时间。虽然软件领域早就有“自动程序修复”，但以前的方法在硬件上要么太慢，要么修出来的东西不够可靠。论文就是想解决这个痛点：把硬件 RTL 自动修复做得[c16471] 既快又实用。

作者把自己的工作和此前代表性工具 CirFix 做了直接对比。论文摘要和引言里强调，RTL-Repair 比 CirFix（2022） 更快，很多修复能在几秒内完成，而不是几分钟甚至几小时；而且修出来的结果整体更正确。

二、论文的核心贡献

这篇文章的贡献可以压缩成四句话：

第一，它提出了一个基于语义和 SMT 求解的 RTL 修复算法，不是随便猜补丁，而是把“哪些地方能改、怎么改”编码成符号变量，让求解器去找满足测试约束的最小修改。

第二，它提出了一个很关键的技术：adaptive windowing，自适应窗口化。因为长测试会导致符号展开太大、太慢，所以它不一次把整个测试全展开，而是围绕 bug 暴露的时间点，只看最相关的一小段，并且按需要逐步扩展窗口。

第三，它引入了一个分析 bug 难度的指标：OSDD（output/state divergence delta）。这个指标看的是：内部状态第一次出错，到外部输出第一次出错，中间隔了多少步。这个值越大，通常 bug 越难修，因为错误藏得更深。

第四，它做了系统实验，既比较了 RTL-Repair 和 CirFix，也拿开源项目里的真实 bug 来测试，说明方法不仅在论文 benchmark 上有效，也有一定真实场景价值。

三、你必须先懂的背景概念

1. 什么是 RTL

RTL 是数字电路设计里的一个抽象层次。工程师在这一层用 Verilog/SystemVerilog 这类 HDL 去描述：寄存器、存储器在每个时钟周期怎么更新。后面的综合工具再把 RTL 变成低层电路实现。论文强调，大多数逻辑 bug 都是在 RTL 这一层暴露出来的。

2. 什么是 testbench / I/O trace（追踪）

修复工具需要知道“哪里错了”。这里作者用的是测试轨迹：也就是每个周期输入是什么、期望输出是什么。论文把它写成 I/O trace，本质上就是一个按时钟周期展开的输入输出表。

3. 什么是 BMC

BMC 是 bounded model checking，有界模型检测。它的想法是：把系统展开若干个时钟周期，交给 SAT/SMT 求解器，看是否存在某组输入会导致断言失败。RTL-Repair 借用了这个思想，但不是拿它来“找反例”，而是拿它来“找修复”。

四、这篇论文最核心的思想：把“修 bug”变成一个求解问题

作者用了一个很直观的例子：一个计数器在 reset 时漏掉了对 count 的清零，所以 reset 后输出不是 0。论文在第 3 节用这个例子展示了整个修复思路。

它的流程可以这样理解：

先把 Verilog 代码转换成一个状态转移系统，也就是“当前状态和输入，如何决定下一拍状态”的数学表达。论文中借助 yosys，把 Verilog 变成 SMT 可处理的形式。

然后不是直接修改原代码，而是先往代码里插入一些“可能的修复位置”和“可选修改模板”。比如：

• 某个地方可不可以加一条赋值；
• 某个条件可不可以取反；
• 某个常数可不可以换掉。

这些修改都不是立刻生效，而是由一些符号变量控制。也就是：让求解器决定改不改、改哪里、改成什么。

接着，把测试轨迹也编码进去，要求修复后的电路在这些输入下必须产生正确输出。这样一来，问题就变成：

是否存在一组修改选择，使得电路通过测试？

如果存在，再进一步要求：

在所有可行修复中，修改数量最少的是哪个？

这个“最小修改”非常关键。因为改得越少，越不容易误伤没测到的功能，也越容易让人理解。论文明确说，最小化修改数有两个好处：更容易泛化到别的测试，也更方便开发者人工确认。

五、RTL-Repair 用了哪三类修复模板

论文的模板设计是重点，老师也很可能会问。

1. Replace Literals

就是替换常数字面量。
例如代码里写了一个错误的 2'd1、4'b1000 之类，工具允许把这些常数替换成一个由求解器决定的新值。但不是所有常数都能替，因为有些地方要求编译期常量，随便换会破坏可综合性。作者只在安全的位置替换。

2. Add Guard

就是给条件或 1-bit 表达式增加保护条件，或者反转条件。
比如原来某个条件少了一个限制，就可能需要再加一个 && something；或者某个 if 的判断方向写反了，就可能需要取反。作者还特别处理了组合环路问题，避免因为乱加条件导致电路不可综合。

3. Conditional Overwrite（条件覆盖）

就是在 process 的开头或结尾，插入一个新的条件赋值。
它允许给某个信号再补一条赋值，并且这个赋值可以带条件。这个模板特别适合修“漏赋值”“漏 reset”“少更新一次”这类 bug。

你可以先把这三类记成：

• 改常数
• 改条件
• 补赋值

这已经概括了 RTL-Repair 的主要动作空间。

六、论文真正厉害的点：为什么它快

真正让这篇论文有说服力的，不只是“能修”，而是“修得很快”。

如果对整条测试轨迹全量展开，测试越长，求解就越慢。尤其硬件测试常常跨很多时钟周期，这会让 BMC 风格的方法非常吃不消。

作者的解决办法是 adaptive windowing：

先找到第一次输出出错的时间点。
然后一开始只在这个点附近做很小范围的符号展开：前后只看很少几个周期。
如果这个小窗口内找不到正确修复，再分析失败原因，决定是：

• 要向前多看几步，因为真正的状态更新 bug 更早发生；
• 还是向后多看几步，因为当前窗口没有包含足够的未来行为。

这个思路很像人类调 bug：先盯着报错附近看，只有必要时才往前翻。
论文说，有个 benchmark 原本一小时都修不出来，用这个方法后不到十秒就修好了。

七、实验结果说明了什么

这篇论文实验部分结论很明确：

在论文的主 benchmark 上，RTL-Repair 找到了 16 个正确修复，而 CirFix 只有 10 个。

从速度看，RTL-Repair 通常是几秒内给出答案，而 CirFix 常常要几分钟、几小时，甚至超时。论文表 1 的总览就显示：RTL-Repair 的正确修复中位时间约为 0.70 秒，CirFix 则是 2.53 分钟；很多情况下 CirFix 甚至达到数小时量级。

作者还强调，不是所有“通过 testbench”的修复都是真的好修复。有些方法只是让仿真过了，但会带来综合-仿真不一致，也就是仿真看似正确，真正综合成电路后行为可能不一样。RTL-Repair 在评价时加入了 gate-level simulation 等检查，强调修的不只是“Verilog 表面行为”，而是更接近真实硬件的正确性。

另外，在 12 个来自开源项目的真实 bug 上，RTL-Repair 能让其中 9 个 通过测试，但作者也很诚实地说：真实项目里的 testbench 往往覆盖不足，所以有些修复虽然能过测试，但未必完全等同于 ground truth。

八、这篇论文的优点和局限

优点

它最大的优点有三个。

第一，快。很多结果在秒级返回，具备以后做 IDE 辅助修复的可能。

第二，改动小。它追求 minimal repair，不容易把无关代码一起改坏。

第三，更考虑真实硬件语义。它避免只修仿真、不顾综合结果的问题。

局限

它也不是万能的。

比如某些 bug 会从根本上改变综合出来的电路结构，这类问题它就不擅长。论文举了 counter_w1 的例子，像 sensitivity list / posedge 这种错误，会改变“这是时序逻辑还是组合逻辑”，RTL-Repair 因为直接工作在综合后的电路语义上，反而不容易修这种 bug。

再比如，如果 testbench 太弱，工具可能找到“过拟合测试”的修复，而不是真正通用的修复。作者在开源 bug 实验中也承认了这个问题。

九、你可以怎么向老师概括这篇论文

你可以用这一段来口头复述：

这篇论文提出了 RTL-Repair，一个面向 Verilog RTL 代码的自动修复工具。它把可能的代码修改编码成符号化模板，再结合测试轨迹和 SMT 求解器，搜索能让电路通过测试的最小修改。为了应对长测试带来的求解开销，论文提出了 adaptive windowing，只在 bug 附近做局部符号展开，并按需扩展窗口。实验表明，它比此前的 CirFix 修得更快、正确修复更多，而且更注意避免综合与仿真不一致的问题。

十、第一轮读完，你现在至少要记住这 5 个点

1. 研究问题：自动修 RTL 硬件代码中的 bug。
2. 关键方法：修复模板 + SMT 求解 + 最小修改。
3. 三类模板：改常数、改条件、补赋值。
4. 加速关键：adaptive windowing。
5. 实验结论：比 CirFix 更快，正确修复更多。