Skip to content
Preprint

SpecLens: LLM-Based Verilog Generation with Specification-Derived Constraints via Behavioral Divergence

Sep 2026 · 0 citations · 26 references
Computer Science

TL;DR

This work proposes SpecLens, an automated framework for LLM-based Verilog generation that derives specification-driven constraints by analyzing behavioral divergence among multiple candidate implementations, using the original specification as the only external semantic source during generation.

Abstract

Large language models (LLMs) have recently shown promise in Verilog generation, but producing functionally correct RTL directly from natural-language specifications remains a highly challenging task. Existing approaches improve LLM-based Verilog generation mainly with retrieval-augmented generation (RAG), self-planning, or few-shot prompting. However, these methods focus primarily on external or generic forms of enhancement rather than strengthening the specification with task-specific constraints. In this work, we propose SpecLens, an automated framework for LLM-based Verilog generation that derives specification-driven constraints by analyzing behavioral divergence among multiple candidate implementations, using the original specification as the only external semantic source during generation. On the VerilogEval v2.0 spec-to-RTL benchmark, SpecLens achieves a functional pass@1 ratio of 86.2\% with o3-mini-medium and 89.4\% with o3-mini-high. This corresponds to a 3.6 percentage-point gain over the SOTA prompting method with o3-mini-medium and a 3.8 percentage-point gain over the SOTA behavioral divergence method with o3-mini-high. In addition, on RTLLM v1.1 and v2.0, analysis shows that SpecLens is more specification-faithful and less prone to benchmark-aligned priors. SpecLens achieves 100\% syntactic correctness on VerilogEval v2.0, 86.2\% on RTLLM v1.1, and 88\% on RTLLM v2.0, even without using costly compile-repair loops to revise generated code iteratively. The code is open source and available at https://anonymous.4open.science/r/SpecLens-4632/readme.md.

View source

Similar papers

#small language model Preprint Sep 2026

Path2Spec: Path-Aware Specification Generation via Large Language Models

This work introduces Path2Spec, a divide-and-conquer framework that leverages LLMs to extract all execution paths from an input program, generates path-specific specifications for each, and merges them into a comprehensive overall specification.

Dan Huang, Zhensu Sun, Hui-Hui Huang et al. · 0 citations
Book Open access Oct 2026

A Transformation-Based Benchmark for Evaluating the Robustness of LLMs in Generating OCL

A transformation-based benchmarking approach for OCL generation is introduced, based on deterministic, semantics-preserving UML model transformations; such as identifier renaming, attribute reification, and association reification, that preserve specification intent while altering model representation.

Hamza Attarwala, Moataz Chouchen, Omar Alam et al. · 0 citations
Preprint Aug 2026

NoTB: Oracle-Free Triage of LLM-Generated RTL via Cross-Model Formal Consensus

NoTB is introduced, an oracle-free triage framework that infers correctness from cross-model formal consensus and demonstrates that formal cross-model agreement provides a reliable basis for high-confidence triage without model-dependent oracles.

Elisavet Lydia Alvanaki, Je Yang, Biruk B. Seyoum et al. · 0 citations
Conference Open access Sep 2026

QiMeng-VPID: Verification-Grounded Port-Level Iterative Decomposition for Complex Verilog Generation

This work proposes VPID, a multi-agent framework for generating complex Verilog that achieves monotonic functional improvement and introduces an experience-guided refinement strategy that distills historical waveform mismatches into constraints, guiding the targeted debugging for the unverified ports.

Hong-Guang Wang, Jiaming Guo, Rui Zhang et al. · 0 citations

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.