Pith. sign in

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

arxiv 2507.10338 v1 pith:R77MFT34 submitted 2025-07-14 cs.SE cs.ARcs.LO

AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction

classification cs.SE cs.ARcs.LO
keywords assertcoderassertioncorrectnessevaluationframeworkfunctionalhardwarehigh-quality
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved
0 comments
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.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 4 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications

    cs.AR 2026-05 unverdicted novelty 7.0

    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.

  2. SafeGen: LLM-Driven Assertion Generation and Fault Criticality Evaluation for Functional Safety

    cs.AR 2026-06 unverdicted novelty 6.0

    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...

  3. Autoformalizing Memory Specifications with Agents

    cs.AR 2026-04 unverdicted novelty 6.0

    An agent system autoformalizes industry DRAM specifications into DRAMPyML for verification tasks like assertion generation, with DRAMBench dataset released for benchmarking.

  4. LLM Assisted Verification Assertion Generation: Challenges and Future Directions

    cs.ET 2026-07 conditional novelty 2.0

    A review of LLM-based SystemVerilog Assertion generation frameworks, identifying challenges in specification processing, signal mapping, vacuity, and evaluation, with guidelines for future research.