Wuqian Tang, Fangzhou Liu, Ruijie Wang, TingTing Hwang, Bei Yu, Chun-Yao Wang
原文摘要
Hardware designs may be available only as gate-level netlists or input-output descriptions when the original register-transfer-level (RTL) design and documentation are not accessible. Low-level representations obscure word-level computation and its finite-width behavior. Recovering high-level RTL from such representations therefore helps engineers understand a circuit's functionality and enables RTL rewriting and resynthesis. A plausible function model is also insufficient unless the generated RTL is equivalent to the original circuit for all input combinations. In this paper, we present RTLREX, a large language model (LLM)-guided framework that coordinates domain-specific tools for function recovery, RTL generation, independent verification, and cost-guided rewriting. Independent verification establishes equivalence between the recovered RTL and the original circuit. The LLM uses tool feedback to select further analyses, revise candidate RTL, and propose syntax-cost reductions. Experiments on 30 benchmarks from Problem A of the ICCAD 2022 CAD Contest show that RTLREX recovers equivalent high-level RTL for all benchmarks, surpassing the state-of-the-art method WolFEx in recovery coverage. On benchmarks recovered by both methods, RTLREX reduces mean syntax cost by 20.5% relative to WolFEx. On complete truth-table benchmarks from the IWLS 2026 Contest, our framework reduces mean syntax cost by 95.7% relative to an LLM agent baseline on the benchmarks validated by both methods.
We study proportional fairness in graphical resource allocation, where agents are vertices, indivisible items are edges, and each item must be allocated to one of its two endpoints. It has been proved that PROP1 orientations always exist and PROPx orientations may not, but it has remained open whether the intermediate relaxations PROPm and PROPavg (both can be satisfied without graphical constraints) can always be satisfied. In this paper, we resolve this gap. We prove that PROPm orientations always exist for goods on multigraphs and can be computed efficiently. The guarantee extends to chores and a mixture of goods and chores. In sharp contrast, we show that PROPavg orientations need not exist, even for simple graphs with binary valuations, and that deciding their existence is NP-complete. We further quantify the efficiency loss of PROPm: for goods, the price of PROPm is exactly $2$, which is one of the few settings where a constant bound on the price of fairness can be obtained. We complement these results with hardness results for welfare optimization under PROPm and for the existence of orientations that are simultaneously PROPm and Pareto optimal.