Source-linked AI summary
NeuroAbs: A Neuro-Symbolic RTL Abstraction Framework for Property Checking Acceleration
Zhiyuan Yan, Xiaofeng Zhou, Ziyue Zheng, Ziyi Yang, Wenbin Che, Wei Zhang, Yangdi Lyu, Hongce Zhang
TL;DR
Efficient property checking for complex RTL requires abstractions that are less manual and more flexible than existing approaches. NeuroAbs combines LLM-assisted candidate identification, AST-guided rewriting, SMT soundness checking, and CEGAR refinement, improving formal proof search and bug-finding efficiency across representative verification tasks.
Problem
RTL abstraction remains design- and property-specific, while existing approaches rely on manual effort or inflexible rule-based techniques.
Method
NeuroAbs uses LLMs to identify abstraction candidates and generate AST-constrained rewrites, then applies SMT checking and CEGAR refinement to maintain sound over-approximation.
Results
NeuroAbs accelerates formal proof search and improves bug-finding efficiency with BMC across several representative RTL verification tasks.
Takeaways & Limitations
The framework provides flexible, automated RTL abstraction that improves formal property-verification efficiency across various RTL designs.
Takeaways & Limitations
Sequential abstraction generation causes total runtime to grow linearly, although parallelizing rewrites could provide further speedups.
Abstract
from arXiv · showhide
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 abstraction. It then combines LLM-based abstraction with an AST-based symbolic RTL representation to better align the generated abstraction with the intended transformation. The soundness of each abstraction is checked using satisfiability modulo theories (SMT) solving. If the abstraction is too coarse for a successful proof, NeuroAbs applies counterexample-guided abstraction refinement (CEGAR) to iteratively refine the model. Experimental results show that NeuroAbs significantly improves the efficiency of hardware property checking across a range of verification tasks.
1 Introduction
The introduction frames RTL property checking as increasingly difficult for complex circuits because suitable abstraction is design- and property-specific. NeuroAbs addresses this challenge with an LLM-guided, AST-aligned abstraction flow checked and refined using SMT and CEGAR.
- Motivation: As RTL circuits grow larger and more complex, abstraction simplifies models while preserving behaviors relevant to property verification.Prior approaches include manual abstraction and rule-based automatic abstraction.
- Motivation: Proper abstraction is both design-specific and property-specific, requiring knowledge of the design and the property being checked.For an ADD-instruction property, logic for unrelated AND and subtraction operations can be replaced with free or unknown values.
- NeuroAbs framework: NeuroAbs uses one LLM to analyze design and property intent, identify abstraction candidates, and generate candidate RTL rewritings.The framework is presented as the first work to apply LLMs to RTL abstraction.
- NeuroAbs framework: NeuroAbs aligns generated abstractions with intended transformations by localizing selected statements through a symbolic RTL AST before rewriting designated regions.The symbolic component constrains where the neural component's scenario-aware abstraction is applied.
- Validation: SMT-based soundness checking verifies that each abstraction is a sound over-approximation, while CEGAR refines abstractions that are too coarse.The evaluation covers RISC-V Formal, instruction-level abstraction refinement checking, and an I2C peripheral.
2 Background
The background formulates RTL designs as finite-state transition systems and defines safety checking over reachable states. It also motivates scenario-specific abstraction, noting that functional analysis can reveal opportunities missed by structural methods.
- RTL Modeling: An RTL model is represented as a finite-state transition system with state variables, initial states, and a transition relation.Input variables are treated as free state variables and omitted from the formulation.
- Property Checking: Safety checking determines whether a property holds for every state reachable from the initial states; otherwise, it produces a counterexample trace.
- RTL Abstraction: Abstraction simplifies RTL while preserving an overapproximated state space, with abstract initial states and transitions containing those of the original system.The abstraction is defined so Init |= Î Init and Tr |= Î Tr, making the abstract state space a superset of the concrete one.
- Verification Scenarios: Verification scenarios specify an operational context, assumptions, and properties for a focused configuration or operating mode.Different hardware configurations or modes are typically verified separately with customized setups.
- Scenario-Specific Abstraction: Functional analysis can identify scenario-irrelevant RTL logic that structural techniques such as Cone of Influence may miss, motivating LLM-based relevance identification.For example, verifying an ADD instruction can abstract logic associated with other instructions.
3 Our Method
NeuroAbs combines scenario-aware LLM analysis with RTL static analysis and AST-based symbolic localization to generate constrained abstraction candidates. An Abstractor rewrites selected RTL statements, while SMT soundness checking and CEGAR refinement address invalid or overly coarse abstractions.
- Overview: NeuroAbs uses a three-stage neuro-symbolic flow in which an LLM proposes scenario-aware abstraction candidates and symbolic analysis constrains, validates, and refines them.The flow first identifies relevant signals, then localizes and transforms RTL statements, and finally checks and refines the abstraction.
- Signal Analysis: The Signal Analyzer narrows abstraction scope by combining LLM interpretation of design and verification context with RTL static analysis and dependency tracking.Because lengthy RTL exceeds practical LLM context limits, static analysis localizes logic connected to scenario-related signals; fixed values can also enable constant propagation.
- Signal Analysis: For an ADD scenario, constant propagation from opcode 2′𝑏01 simplifies related assignments such as id_wen and alu_result, identifying statement-level abstraction candidates.The localized candidates are then used to find corresponding AST nodes.
- AST-Based Transformation: AST localization gives each candidate a finite, semantically meaningful rewrite boundary and supplies enclosing constructs such as always, initial, and case blocks as structural context.The Abstractor generates abstractions only at selected statement-level AST nodes rather than unconstrained RTL text spans.
- Validation and Refinement: The Abstractor preserves property-relevant computation while rewriting unrelated parts of localized statements, and SMT checking requires each result to be an over-approximation.If the abstraction remains too coarse and creates spurious counterexamples, NeuroAbs applies counterexample reduction within a customized CEGAR loop to refine the abstract model.
4 Experiment
The experiments evaluate NeuroAbs across abstraction quality, model-checking acceleration, and state exploration using competitive RIC3 and AVR baselines. Results show improved abstraction quality, deeper and faster BMC exploration, efficient refinement, and support for diverse RTL constructs.
- Experimental Setup: NeuroAbs is evaluated on open-source RISC-V processor verification tasks using RIC3 and AVR, competitive HWMCC model checkers.The setup uses Yosys for RTL analysis, Pyverilog for AST conversion, and GPT-4o-mini with 8 few-shot examples.
- RQ1: Abstraction Quality: Removing few-shot learning reduces the correct over-approximation rate to 83.51%, while also removing custom instructions yields 96.46%.The study measures both correct over-approximations and strict over-approximations that are semantically different from the original statements.
- RQ2: Model-Checking Acceleration: In Piccolo, NeuroAbs increases average BMC depth from 109.36 to 125.36 and, in Flute, reduces time to the baseline maximum depth by 75.98%.For Flute, runtime decreases from 23,600 seconds to 5,668.58 seconds.
- Refinement and Overhead: CEGAR refinement averages 7.26 seconds and 1.65 iterations, while LLM rewriting averages 3.70 seconds per statement.Abstractions are generated sequentially, making total LLM runtime longer, but combined inference and refinement still outperform the baseline.
- RQ3: State Exploration: At 10,000 seconds, NeuroAbs reaches depth 161 versus 93 without abstraction; at 20,000 seconds, it reaches 207 versus 121.The widening gap over time reflects reduced complexity in BMC’s unrolled expressions, improving solving efficiency at larger depths.
- Supported RTL Constructs: NeuroAbs abstracts unary and binary operators, multi-statement always blocks, ternary operators, and case statements.These results indicate support for diverse RTL abstraction scenarios guided by the target property.
5 Conclusion
NeuroAbs is presented as a neuro-symbolic framework for flexible, automated RTL abstraction using LLMs and symbolic verification. It combines signal identification, AST-guided abstraction, SMT soundness checking, and CEGAR refinement.
- 5 Conclusion: NeuroAbs uses LLM-assisted RTL analysis to identify signals and statements suitable for abstraction.This enables flexible and automated abstraction for RTL models.
- 5 Conclusion: AST-guided LLM-based abstraction generates an initial abstract RTL model.The AST-based guidance aligns the generated abstraction with the RTL representation.
- 5 Conclusion: SMT checking and CEGAR maintain abstraction soundness and iteratively refine the model when necessary.These mechanisms support sound abstraction refinement during verification.