../

Bridging RTL and Assertion Generation With Large Language Models

Year
2026
Authors
Jayanth Thangellamudi, Sai Manoj Pudukotai Dinakarrao
DOI
10.1109/MDAT.2026.3670060

Related

Persistent Notes

In-text annotations

“Among these, assertion generation is particularly labor-intensive and error-prone, often acting as a bottleneck that delays downstream verification." Page 5

“Despite these advances, current LLM-based approaches remain task-specific and fragmented; some target RTL generation [2], whereas others focus solely on assertion generation [5]. The absence of integration across these two tightly coupled processes leads to: 1) inconsistency between RTL and assertions; 2) limited scalability due to poor task generalization; and 3) weak domain adaptation, as hardware-specific constraints are not embedded deeply into the learning process." Page 6

“In Phase I, the model generates semantically consistent RTL modules; in Phase II, it derives SystemVerilog assertions (SVAs) directly from the generated RTL rather than relying on natural-language prompts." Page 6

What is the difference between this and asking the LLM to generate directly seeing a human written RTL vs it’s own? is it the same? Page 6

“Experimental results on the RTLLM benchmark” Page 6

“correctness” Page 6

What correctness? Page 6

“We construct two separate fine-tuning datasets, each containing approximately 26,000 datapoints:" Page 8

“Each datapoint is represented as an instruction–implementation pair, where instructions are handcrafted, template-generated, or extracted from HDL documentation, and Verilog implementations are sourced from open-source codebases or rule-based synthesis." Page 8

“The SVA dataset is constructed independently to fine-tune SVA generation." Page 8

“SVAs are either manually authored by domain experts or generated using LLM-assisted workflows to ensure semantic consistency with the RTL." Page 8

“As shown in Table 2, Stage 2 achieves 88% syntactic validity, with 21 out of 30 designs producing functionally meaningful assertions formally verified using JasperGold." Page 12

Does 21/30 mean that in 21 designs all the assertions pass? Does having one failing assertion mean that the design fails? Page 12

“domain-specific adaptation” Page 12

What is this? Page 12

%% Import Date: 2026-06-25T14:19:49.747-04:00 %%