Gate-level netlists become readable RTL: RTLREX recovers equivalent designs for all 30 contest benchmarks
Synopsis
When the original RTL and documentation are gone and only a gate-level netlist or a complete truth table remains, RTLREX has a large language model choose analyses among domain-specific tools, build candidate RTL, and confirm each result with independent equivalence checking. On the 30 benchmarks of ICCAD 2022 CAD Contest Problem A it recovered equivalent high-level RTL for all of them, above WolFEx's 26, and on the 26 recovered by both it cut mean syntax cost by 20.5% relative to WolFEx.
Interpretation
RTLREX turns a gate-level netlist or a complete truth table into synthesizable high-level RTL, and every candidate passes independent equivalence checking rather than only simulation on sampled vectors. Earlier arithmetic-recovery methods Hybrid-DATE and WolFEx report recovery on 23 and 26 of the 30 ICCAD 2022 CAD Contest Problem A benchmarks, so their coverage is incomplete. All 30 benchmarks pass equivalence proof and RTL validity checking; on the 26 recovered by both RTLREX and WolFEx, mean syntax cost falls from 14.04 to 11.15, a 20.5% reduction, with 6 lower and 20 equal.
A large language model reads circuit observations and tool feedback to decide which analysis to run next, and after equivalence is established proposes rewrites that lower syntax cost. Automatic recovery tools match predefined function models in sequence, and a mismatch calls for additional circuit analysis and revision of candidate expressions. On test27 automatic recovery first produced no word-level candidate; the model used dependency analysis and simulation to build conditional arithmetic expressions, then boundary probes where operand sums of 511 and 512 distinguished a signed 10-bit intermediate, and the result passed exact equivalence checking.
For multiplication-rich netlists that resist conventional bit-level equivalence checking, verification is split into smaller independently proved tasks and then composed. Direct combinational equivalence checking or bit-vector satisfiability checking of the whole netlist can end inconclusive. Complete-interface proofs across the 30 benchmarks comprise 15 direct CEC proofs, 6 arithmetic proofs and 9 combined proofs, plus one bit-vector SMT check that independently verifies test23, totaling 31 proofs over 30 distinct benchmarks.
Perspective
The evaluation covers the 30 combinational primitive-gate netlists of ICCAD 2022 CAD Contest Problem A and the 100 complete truth tables ex200–ex299 from the IWLS 2026 Contest, with 8–16 input bits and 4–32 output bits; the truth-table syntax-cost weights are adapted from the PA-30 contest weights for this work and are not part of the official IWLS scoring rules. Area and delay are pre-layout estimates using the Nangate45 library, a 2 ns delay target and OpenSTA, excluding placement and extracted interconnect parasitics.
Syntax cost measures source-level compactness only, and a lower cost does not guarantee lower synthesized area or delay; resynthesis gains depend on the circuit and synthesis flow, as test06 shows an 18.7% delay reduction with a 12.2% area increase. Twenty truth-table benchmarks still yield only bit-level Boolean RTL without exposed word-level structure, and one of the 100 TT-100 runs reached the 600-s generation time limit.