NeuroAbs: A Neuro-Symbolic RTL Abstraction Framework for Property Checking Acceleration
Formal verification is a crucial technique for ensuring the functional correctness of hardware designs. In the context of property checking, a key challenge is how to efficiently prove a user-specified property in the face of increasingly complex RTL designs. To address this challenge, abstraction techniques are often employed to reduce system complexity and accelerate the verification process. However, prior RTL abstraction methods either require significant manual effort or rely on rule-based techniques that lack flexibility. This paper introduces NeuroAbs, a neuro-symbolic framework for RTL abstraction. NeuroAbs first uses LLM-assisted RTL analysis to identify signals suitable for abst...
| Authors | Zhiyuan Yan, Xiaofeng Zhou, Ziyue Zheng et al. |
|---|---|
| Primary category | cs.AR |
| Published | 18 August 2026 |
| Last updated at source | 18 August 2026 |
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 17 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.