REVIEW 4 cited by
AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction
read the original abstract
Assertion-Based Verification (ABV) is critical for ensuring functional correctness in modern hardware systems. However, manually writing high-quality SVAs remains labor-intensive and error-prone. To bridge this gap, we propose AssertCoder, a novel unified framework that automatically generates high-quality SVAs directly from multimodal hardware design specifications. AssertCoder employs a modality-sensitive preprocessing to parse heterogeneous specification formats (text, tables, diagrams, and formulas), followed by a set of dedicated semantic analyzers that extract structured representations aligned with signal-level semantics. These representations are utilized to drive assertion synthesis via multi-step chain-of-thought (CoT) prompting. The framework incorporates a mutation-based evaluation approach to assess assertion quality via model checking and further refine the generated assertions. Experimental evaluation across three real-world Register-Transfer Level (RTL) designs demonstrates AssertCoder's superior performance, achieving an average increase of 8.4% in functional correctness and 5.8% in mutation detection compared to existing state-of-the-art approaches.
Forward citations
Cited by 4 Pith papers
-
AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications
AssertLLM2 introduces a benchmark of 83 designs supporting bug-prevention and bug-hunting assertion generation tasks with evaluation across syntactic, formal, coverage, and mutation-based metrics.
-
SafeGen: LLM-Driven Assertion Generation and Fault Criticality Evaluation for Functional Safety
SafeGen combines LLMs with a document-level HyperKG and formal property verification to generate traceable functional safety assertions and assess fault criticality more interpretably than prior LLM generators or simu...
-
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.
-
LLM Assisted Verification Assertion Generation: Challenges and Future Directions
A review of LLM-based SystemVerilog Assertion generation frameworks, identifying challenges in specification processing, signal mapping, vacuity, and evaluation, with guidelines for future research.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.