Validatable Generation of System Verilog Assertions from Natural Language Specifications

We present a novel approach for automatically converting natural language specifications into validated formal System Verilog Assertions (SVAs) using fine-tuned large language models. In addition, we propose a validation algorithm that analyzes each candidate assertion based on its syntactic and semantic compatibility with the original English specification. In order to accomplish this, we build and fine-tune a second language model to convert the generated SVA back to an English statement. Because this generated English statement may not exactly match the original spec, we generate another SVA using this new English statement to check if the SVA matches the one generated in the first step. Experimental results show that 92% of the spec were correctly converted to the corresponding SVAs.