一句话:提出基于SMT的RTL硬件设计快速符号修复工具,可在秒级生成最小修复并适配IDE。
RTL 电路描述的调试与修复通常依赖人工或耗时搜索,现有最优工具生成修复需数分钟甚至数小时。RTL-Repair 是一个基于语义的寄存器传输级电路修复工具,采用 SMT 的一步式故障定位与修复算法,并通过优化生成用户易理解的最小改动;其自适应窗口方法将修复搜索聚焦于测试中最相关的部分,以缓解可扩展性问题。在从开源硬件项目收集的 12 个真实 bug 上,RTL-Repair 为其中 9 个生成了能通过测试平台的修复:2 个与真实修复完全一致,1 个部分一致,4 个改对了表达式但过拟合测试平台,仅 3 个与真实修复差异较大。
We present RTL-Repair, a semantics-based repair tool for register transfer level circuit descriptions. Compared to the previous state-of-the-art tool, RTL-Repair generates more correct repairs within seconds instead of minutes or even hours. We imagine that RTL-Repair could thus be integrated into an IDE to give developers repair suggestions promptly. Our new SMT-based one-step fault localization and repair algorithm for digital hardware designs uses optimization to generate minimal changes that a user can easily understand. A novel adaptive windowing approach allows us to avoid scalability issues by focusing the repair search on the parts of the test that matter the most. RTL-Repair provides repairs that pass their testbench for 9 out of 12 real bugs collected from open-source hardware projects. Two repairs fully match the ground truth, one partially, four more repairs change the correct expression but in a way that overfits the testbench, and only three repairs differ strongly from the ground truth.
@inproceedings{LaeuferFAINS24,
title = {RTL-Repair: Fast Symbolic Repair of Hardware Design Code},
author = {Kevin Laeufer and Brandon Fajardo and Abhik Ahuja and Vighnesh Iyer and Borivoje Nikolić and Koushik Sen},
booktitle = {ASPLOS},
year = {2024},
doi = {10.1145/3620666.3651346}
}