Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting

TL;DR

This work presents a large language model -based flow to automatically generate high-quality SVA from the design specification documents, and introduces 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.

Abstract

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.

Figures (4)

• Figure 1: The proposed AssertCraft full-stack flow employs two novel techniques—sub-tasked fine-tuning, and iterative prompting—to produce high-accuracy assertion statements from the specification document. Moreover, this flow was completed by adding an additional dataset and scoreboard for assessing the ability of the model to generate high-quality assertions.
• Figure 2: Comparison of assertion generation across three scenarios: employing Plain GPT alone, modifying Plain GPT with comments extracted via the first phase of Sub-task Focused Fine-tuning, and AssertCraft which includes a custom GPT for assertion generation and comment extraction. All these models also include the iterative prompting method to fix syntax and semantic errors.
• Figure 3: The quality of the generated assertions for each design in the HDLBits dataset hdlbits is represented in a bar chart. The red bar indicates the number of assertions with syntax or semantic errors. The blue bar illustrates the number of functionally incorrect assertions. Finally, the yellow bar shows the number of functionally correct assertions.
• Figure 4: Coverage results for each HDLBits category hdlbits are shown as distributions. Coverage is represented as a range of values due to multiple designs, with individual data points also included.