Hybrid-NL2SVA: Integrating RAG and Finetuning for LLM-based NL2SVA

--SystemV erilog Assertion s ( SV As) are critical for verifying the correctness of hardware designs, but manually writing them from natural language property descriptions, i.e., NL2SV A, remains a labor-intensive and error-prone task. T o enhance LLM performance in NL2SV A, we propose a customized retrieval-augmented generation (RAG) framework and a synthetic fine-tuning dataset that together improve LLM's performance. Our RAG framework (i) constructs a context-preserving database via dynamic splitting technique, (ii) combines global semantic retrieval with keyword-guided retrieval to extract SV A operator-related contexts via HybridRetrieval, and (iii) validate and correct the use of SV A operators in LLM-generated SV As via SV A operator-based rechecking . T o further improve lightweight models over NL2SV A, our fine-tuning dataset provides prompt-guided explanation s that teach LLMs the layer-by-layer construction process of concurrent SV As, enabling supervised fine-tuning that greatly improves syntax and functionality accuracy. T o evaluate the performance of LLMs over NL2SV A, we construct the largest evaluation dataset for NL2SV A, comprising 40 V erilog designs and 229 formally verified SV As with detailed annotations. Experimental results show that our customized RAG framework increases the number of functionality matched SV As by 58. SystemV erilog Assertion s ( SVAs) are essential tools in hardware verification, formally specifying expected design behaviors, namely the design properties, and serving as embedded checkers that continuously validate the implementation against its specification [1], [2]. However, writing SV As manually is difficult, which consists of two sub-tasks [3], [4]. The first task is to extract intended properties, described in natural language, from hardware designs and detailed specification documents. Once these are identified, the second task is to implement these natural language properties as SV As, i.e., the NL2SV A task.