BRIDGE is presented, a structured prompting framework that decomposes verification into three interconnected domains: Code (implementations), Specifications (formal intent), and Theorem State-ments (constructive correctness claims), and elicits domain-specific intermediate reasoning to connect them.
The results indicate that functional correctness in code generation can be meaningfully improved without modifying the backbone architecture, by jointly optimizing how tasks are prompted, how the model is adapted, and how final outputs are selected.
Large language models can generate register-transfer-level (RTL) designs directly from natural language specifications. Their failures, however, arise mostly from understanding rather than coding \cite{zhang2026understanding, qiu2025towards}. A specification is informal and ambiguous, the model's interpretation stays implicit, and every misreading is committed silently into Verilog, where only simulation can expose it. Intermediate representations make the interpretation partly explicit, yet existing works don't verify the interpretation against the specification, and repair simulation failures at the code level regardless of where the misreading originated. VeriRefine instead treats specification refinement as a verifiable stage of RTL generation. It progressively refines the prose specification into an explicit, schema-constrained account of design intent, expressed as per-signal Abstract Signal Transition Functions (ASTFs) that commit each signal's logic style, clock domain, and reset behavior before any code exists and ground every behavior in a verbatim specification sentence. The refined specification then passes a five-layer audit spanning soundness, completeness, consistency, FSM integrity, and core RTL design rules, so interpretation errors are repaired at the representation level before any Verilog is generated. Once code is generated, each simulation failure is classified as an understanding error or a coding error and routed back to the corresponding stage for targeted repair. Because every signal's hardware class is fixed during refinement, synthesizability becomes a structural property of the pipeline rather than a post-hoc check. With Claude Sonnet 4.6, VeriRefine reaches 94.0\% functional correctness on RTLLM v2.0 and 98.1\% on VerilogEval-Human v2.
Xiangfei Kong, Tasnim Tabassum, Marwan Abdelwahab et al.· 0 citations
This work addresses three interconnected challenges in building behaviorally-grounded code generation: retrieving not just what symbols are, but how they behave through usage patterns; adapting practices across contexts by separating behavioral intent from implementation details; and enforcing semantic properties during generation without prohibitive runtime costs.
A test-driven pipeline is presented that extracts functional requirements (FR) from a problem description, resolves dependencies, maps them into a modular Model-View-Controller (MVC) structure, and generates tests before code, followed by bounded, execution-driven refinement.
Wasay Mohammed Abdul, Ragib Shahariar Ayon, Shibbir Ahmed et al.· SIGSOFT FSE Companion· 0 citations
This paper introduces SpecCoder, a verification-guided CodeLLM training framework that learns from validated reference programs, behavior-changing mutants, and multi-turn specification-refinement traces, and improves checkpoint-specification quality over base CodeLLMs, and introduces HumanExec, a benchmark built from recent Codeforces competitive programming problems.
Minh Le-Anh, Cuong Chi Le, Tien N. Nguyen· 0 citations
BeSpec is presented, a behavioral model-based approach to specification alignment that treats the task description as partial evidence about the intended behavior of the correct program, and first builds an explicit behavioral model, which are checkable properties that valid outputs must satisfy.
Qinghua Xu, Guancheng Wang, Boxi Yu et al.· 0 citations