2024/11/23 by Mohammad Shahidzadeh, Behnam Ghavami, Shahidzadeh, Mohammad +5
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Handwritten Text Recognition Techniques #Hardware Architecture (cs.AR) #Natural Language Processing Techniques #Speech Recognition and Synthesis
paper · pdf · doi:10.48550/arxiv.2411.15442
openalex publication_date 2024/11/23 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Formal Property Verification (FPV), using SystemVerilog Assertions (SVA), is crucial for ensuring the completeness of design with respect to the specification. However, writing SVA is a laborious task and has a steep learning curve. In this work, we present a large language model (LLM) -based flow to automatically generate high-quality SVA from the design specification documents, named \ToolName. We introduce a novel sub-task-focused fine-tuning approach that effectively addresses functionally incorrect assertions produced by baseline LLMs, leading to a remarkable 7.3-fold increase in the number of functionally correct assertions. Recognizing the prevalence of syntax and semantic errors, we also developed an iterative refinement method that enhances the LLM's initial outputs by systematically re-prompting it to correct identified issues. This process is further strengthened by a custom compiler that generates meaningful error messages, guiding the LLM towards improved accuracy. The experiments demonstrate a 26% increase in the number of assertions free from syntax errors using this approach, showcasing its potential to streamline the FPV process.