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.
Figures & tables
Figure 1. An example of abstraction based on the high-level information of the given property. In this example, OP_ADD , OP_AND and OP_SUB are three different parameters, where OP_ADD=2′b01 , OP_SUB=2′b10 , and OP_AND=2′b11 .
Figure 2. An overview of NeuroAbs.
Figure 3. The custom instruction, COT prompt and response of the Signal Analyzer.
Figure 4. The example of constant propagation. After we assign a constant value to inst , the signal op is set to OP_ADD ( 2′b01 ). Following the constant propagation, id_wen and alu_result will evaluate to 1′b1 and val[rs1]+val[rs2] .
Figure 5. The custom instruction, prompt and response of the Abstractor.
Figure 6. An example of counterexample reduction for our abstract model. When the target property is violated, assignments can be extracted. The reduced counterexample is highlighted in red.
Source Benchmarks
Verification Task
Number of Scenarios
# RTL Lines
# Input Vars
# State Vars
PicoRV32
Generic Inst.-specific
8
3079
82
209
Piccolo
Generic Inst.-specific
22
14943
219
381
Flute
Generic Inst.-specific
22
17228
279
407
I2C
Reg-interface
3
1257
157
47
Table 1. The statistics of benchmark designs in the experiment.
OA rate
Degradation
# avg. strict OA
Degradation
NeuroAbs
95.27%
-
236.17
-
w.o. few-shot
83.51%
12.34%
136.00
42.41%
w.o. few-shot & custom inst.
96.46%
-1.25%
3.83
98.38%
Table 2. Ablation study of NeuroAbs
Design ∗
Runtime (s)
With NeuroAbs
Baseline †
Time to Reach Baseline Max Depth (s)
Improvement (%)
Piccolo
23600
125.36
109.36
15482.67
34.40%
Flute
225.09
129.00
5668.58
75.98%
Table 3. Average unrolling depths explored by BMC w./w.o. NeuroAbs.
Benchmark
Verification Task
# Variable Index (w./w.o. Abstraction)
Total LLM time (s) ∗
Avg. LLM time / stmt (s)
CEGAR time (s)
# CEGAR Iter
# Bound with NeuroAbs
# Bound Baseline
Time to Reach Baseline Max Bound (s)
Improvement (s)
Piccolo
OR-ILA
118188 /129316
361.79
4.41
2.88
2
99
87
15378.68
34.84%
ANDI-ILA
116128 /119628
275.80
3.40
4.05
3
123
106
14126.45
40.14%
JAL-ILA
111567 /116969
305.72
3.40
0.62
1
190
163
13982.43
40.75%
LUI-ILA
111546 /115882
274.46
3.19
5.79
3
200
180
15396.60
34.76%
Flute
SUB-ILA
299217 /1273706
632.07
2.13
6.83
1
221
138
6978.98
70.43%
XORI-ILA
295565 /1272600
611.42
2.09
13.77
1
224
133
5351.54
77.32%
Table 4. Experiment results on representative cases for BMC with or without NeuroAbs.
Figure 7. The runtime (measured in seconds) comparison of reaching a formal proof with or without NeuroAbs. The mean values are: AVR = 607.03, AVR w. NeuroAbs = 334.56; RIC3 = 18.71, RIC3 w. NeuroAbs = 16.94.
Figure 8. Comparison of Depth vs. Time relationship between BMC with and without NeuroAbs across three representative examples.
Type
Before NeuroAbs
After NeuroAbs
Unary
c = ∼ a;
c = ’bx;
Binary
out = a & b;
out = ’bx;
Ternary
out = (PIPELINED) ? a+ b : a - b;
out = (PIPELINED) ? a+ b : ’bx;
Case
case (inst) begin 1’b1: result = a || b; 1’b0: result = a*b; end
case (inst) begin 1’b1: result = a || b; 1’b0: result = ’bx; end
For
for (i = 0; i <32; i = i+1) regs = 0;
for (i = 0; i <32; i = i+1) regs = ’bx;
Always
always @( posedge clk) begin compare <= |{beq, bne}; ari <= |{add, sub} ; end
always @( posedge clk) begin compare <= |{beq, bne}; ari <= ’bx ; end
State Key Laboratory of Novel Software Technology, Nanjing University, China · School of Computer Science, Nanjing University, China · Department of Computer Science, ETH Zurich, Switzerland +1