Formal property checking has been constrained to manually-curated RTL submodules in most industrial flows because state-space explosion makes full-design verification intractable. NeuroAbs attacks that bottleneck from a different angle: use an LLM to identify which RTL signals are candidates for abstraction, generate the abstracted version, then run SMT to certify each abstraction is sound before applying it. If the LLM proposes an abstraction that introduces spurious counterexamples, SMT catches it and the framework refines. The paper is accepted at ICCAD 2026.
The neuro-symbolic split matters here. The LLM handles structural pattern recognition (which signals are likely abstractable given their connectivity and role) via an AST-based RTL representation. SMT handles the soundness claim. The LLM never asserts correctness directly. This is different from prior ML-for-verification approaches that tried to replace the solver with learned heuristics and failed when the learned model generalized badly. NeuroAbs keeps the proof machinery while automating the most manual part of the setup.
The practical bottleneck in formal verification is not solver speed on small designs. It is the engineering time to decompose a complex RTL block into something the solver can handle: writing environment constraints, decomposing properties, manually abstracting irrelevant state. If NeuroAbs reduces that setup cost substantially, verification teams get to run formal on more of the design, earlier, without waiting for a senior formal engineer to wrangle the configuration. That is the shift worth tracking when the ICCAD results are presented. The open question is how it holds up on post-synthesis netlists versus clean RTL; the industrial gap is usually there.