SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation

• URL: http://arxiv.org/abs/2605.25181v1
• Date: Sun, 24 May 2026 17:22:09 GMT
• Title: SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation
• Abstract summary: SpecAlign is a framework for semantic evaluation and refinement of SystemVerilog Assertions.<n>We show that SpecAlign effectively detects semantic inconsistencies and improves assertion alignment without relying on golden RTL.
• Score: 6.0174402828965725
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Weave of Formal Thought [51.56484100374058]
  We introduce Weave of Formal Thought (WoFT), a paradigm uniting rigorous syntactic validation with learned structural representations.<n>We present a latent-variable fine-tuning method training the language model to interleave non-terminal grammar symbols directly into generation.<n>For Python, fine-tuning StarCoder2-3B with our RWS objective reduces per-token cross-entropy by 14.3% relative to a text-only SFT baseline.
  arXiv  Detail & Related papers  (2026-06-24T15:58:11Z)
• Reward-Guided Semantic Evolution for Test-time Adaptive Object Detection [82.2968697030677]
  Open-vocabulary object detection with vision-language models (VLMs) such as Grounding DINO suffers from performance degradation under test-time distribution shifts.<n>We propose Reward-Guided Semantic Evolution (RGSE), a training-free framework that directly refines the text embeddings at test time.
  arXiv  Detail & Related papers  (2026-05-06T06:17:41Z)
• FACTOR: Counterfactual Training-Free Test-Time Adaptation for Open-Vocabulary Object Detection [63.91351553178842]
  FACTOR is a training-free Test-time adaptation for Open-vocabulary object detection.<n>It quantifies attribute sensitivity, semantic relevance, and prediction variation to selectively suppress attribute-dependent predictions.<n>Experiments on PASCAL-C, COCO-C, and FoggyCityscapes show that FACTOR consistently outperforms prior TTA methods.
  arXiv  Detail & Related papers  (2026-05-05T02:31:18Z)
• From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation [0.0]
  SystemVerilog Assertions (SVA) are essential for formal verification of digital hardware.<n>Recent studies have explored using large language models (LLMs) to automate SVA generation.<n>This paper presents ProofLoop, a tool-augmented ReAct agent that generates SVA from natural-language specifications.
  arXiv  Detail & Related papers  (2026-04-25T01:46:33Z)
• SCALE: Semantic- and Confidence-Aware Conditional Variational Autoencoder for Zero-shot Skeleton-based Action Recognition [4.853241666510524]
  Zero-shot skeleton-based action recognition (ZSAR) aims to recognize action classes without any training skeletons from those classes.<n>We propose a lightweight and deterministic Semantic- and Confidence-Aware Listwise Energy-based framework that formulates ZSAR as class-conditional energy ranking.
  arXiv  Detail & Related papers  (2026-04-02T16:12:42Z)
• VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning [4.3414302048068745]
  We present a neurosymbolic framework that combines Large Language Models with SMT solvers to produce verification-guided answers.<n>We introduce three key innovations: (1) multi-model consensus via formal semantic equivalence checking, (2) semantic routing that directs different claim types to appropriate verification strategies, and (3) precise logical error localization via Minimal Correction Subsets.<n>With the GPT-OSS-120B model, VERGE demonstrates an average performance uplift of 18.7% at convergence across a set of reasoning benchmarks compared to single-pass approaches.
  arXiv  Detail & Related papers  (2026-01-27T20:59:11Z)
• AQAScore: Evaluating Semantic Alignment in Text-to-Audio Generation via Audio Question Answering [97.52852990265136]
  We introduce AQAScore, a backbone-agnostic evaluation framework that leverages the reasoning capabilities of audio-aware large language models.<n>We evaluate AQAScore across multiple benchmarks, including human-rated relevance, pairwise comparison, and compositional reasoning tasks.
  arXiv  Detail & Related papers  (2026-01-21T07:35:36Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  We develop CompassVerifier, an accurate and robust lightweight verifier model for evaluation and outcome reward.<n>It demonstrates multi-domain competency spanning math, knowledge, and diverse reasoning tasks, with the capability to process various answer types.<n>We introduce VerifierBench benchmark comprising model outputs collected from multiple data sources, augmented through manual analysis of metaerror patterns to enhance CompassVerifier.
  arXiv  Detail & Related papers  (2025-08-05T17:55:24Z)
• AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction [32.14733357890831]
  We propose AssertCoder, a novel unified framework that automatically generates high-quality SVAs.<n>AssertCoder employs a modality-sensitive preprocessing to parse heterogeneous specification formats.<n>The framework incorporates a mutation-based evaluation approach to assess assertion quality.
  arXiv  Detail & Related papers  (2025-07-14T14:43:14Z)
• Localizing Factual Inconsistencies in Attributable Text Generation [74.11403803488643]
  We introduce QASemConsistency, a new formalism for localizing factual inconsistencies in attributable text generation.<n>We show that QASemConsistency yields factual consistency scores that correlate well with human judgments.
  arXiv  Detail & Related papers  (2024-10-09T22:53:48Z)
• Likelihood-Aware Semantic Alignment for Full-Spectrum Out-of-Distribution Detection [24.145060992747077]
  We propose a Likelihood-Aware Semantic Alignment (LSA) framework to promote the image-text correspondence into semantically high-likelihood regions. Extensive experiments demonstrate the remarkable OOD detection performance of our proposed LSA, surpassing existing methods by a margin of $15.26%$ and $18.88%$ on two F-OOD benchmarks.
  arXiv  Detail & Related papers  (2023-12-04T08:53:59Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.