RTL-BenchLS supplies a large-scale formally verified benchmark and three novel tasks that expose low performance of frontier LLMs on realistic RTL reasoning and generation.
Assertionforge: Enhancing formal verification assertion generation with structured representation of specifications and rtl
5 Pith papers cite this work. Polarity classification is still indexing.
5
Pith papers citing it
years
2026 5representative citing papers
Introduces a quality-aware loop with mutation-guided refinement, RTL-aware solver selection, and causal narrative synthesis to improve LLM-generated assertions for formal verification of RTL designs.
An agent system autoformalizes industry DRAM specifications into DRAMPyML for verification tasks like assertion generation, with DRAMBench dataset released for benchmarking.
CoverAssert iteratively improves LLM-generated assertions via syntax-semantic clustering and coverage feedback, yielding 9.57% branch, 9.64% statement, and 15.69% toggle coverage gains on four open-source designs when combined with prior tools.
citing papers explorer
-
RTL-BenchLS: A Large-Scale Benchmark for RTL Reasoning and Generation with Large Language Models
RTL-BenchLS supplies a large-scale formally verified benchmark and three novel tasks that expose low performance of frontier LLMs on realistic RTL reasoning and generation.
-
Closing the Loop on LLM-Generated RTL Assertions with Quality-Aware Formal Verification
Introduces a quality-aware loop with mutation-guided refinement, RTL-aware solver selection, and causal narrative synthesis to improve LLM-generated assertions for formal verification of RTL designs.
-
Autoformalizing Memory Specifications with Agents
An agent system autoformalizes industry DRAM specifications into DRAMPyML for verification tasks like assertion generation, with DRAMBench dataset released for benchmarking.
-
CoverAssert: Iterative LLM Assertion Generation Driven by Functional Coverage via Syntax-Semantic Representations
CoverAssert iteratively improves LLM-generated assertions via syntax-semantic clustering and coverage feedback, yielding 9.57% branch, 9.64% statement, and 15.69% toggle coverage gains on four open-source designs when combined with prior tools.
- From Indiscriminate to Targeted: Functionally Critical Signal-Driven Assertion Generation using LLMs for Efficient RTL Verification