SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation
For hardware verification engineers, SpecAlign offers a scalable method to evaluate and improve semantic correctness of LLM-generated assertions, reducing debugging effort and increasing confidence in the absence of golden RTL.
SpecAlign addresses the challenge of semantic alignment between LLM-generated SystemVerilog assertions and natural language specifications, introducing iterative alignment loops with entailment-based classification and self-consistency voting to detect and refine misaligned assertions without golden RTL. The framework improves assertion alignment and provides a quantitative alignment score.
Existing Large Language Model (LLM) approaches to SystemVerilog Assertion (SVA) generation primarily focus on syntactic validity and formal verification outcomes, while semantic alignment between generated assertions and natural language specifications remains difficult to quantify. As a result, hallucinated or misaligned SVAs can reduce confidence and increase debugging efforts in the absence of golden RTL. This paper presents SpecAlign, a framework for semantic evaluation and refinement of LLM-generated SVAs. SpecAlign introduces two iterative alignment loops that assess both natural language properties and SVAs against the design specification using entailment-based classification. We improve alignment decisions by generating multiple reasoning paths using chain-of-thought prompting and aggregating them via a self-consistency voting mechanism. Misaligned assertions are analyzed to generate actionable feedback for refinement. We further define a quantitative alignment score to measure semantic consistency across iterations. Experimental results demonstrate that SpecAlign effectively detects semantic inconsistencies and improves assertion alignment without relying on golden RTL, providing a scalable complement to traditional formal verification evaluation metrics.