../

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

Year
2026
Authors
Yuchao Wu, Wenji Fang, Jing Wang, Wenkai Li, Ziyan Guo, Zhiyao Xie
DOI
10.48550/arXiv.2605.27472

Related

Persistent Notes

In-text annotations

“Abstract” Page 1

“AssertLLM2 contains 83 real-world designs across 13 functional categories." Page 1

Opencores mostly Page 1

“To the best of our knowledge, AssertLLM2 is the first benchmark to explicitly use buggy RTL as input to evaluate bug-detection capability." Page 1

“1 Introduction” Page 1

Shortcomings of previous work Page 1

“Limitation 1: Unrealistic formulation." Page 1

“Limitation 2: Oversimplified evaluation." Page 1

“largely focus on syntax and FPV results when evaluating generated assertions." Page 1

We know that this is not enough Page 1

“parsed and proven, but they can not determine whether those assertions constrain relevant logic, improve meaningful formal coverage, or detect design errors. In other words, assertions that are syntactically correct and formally provable may still be trivial, vacuous, or weak in practical verification. Consequently, relying on existing benchmarks can overestimate both assertion quality and the practical utility of LLM-generated assertions." Page 1

These are some nitpicks about the table comparing previous works Page 2

“Dataset” Page 2

What does dataset indicate here? VERT and AssertLLM are finetuned models. While FVEval is a benchmark. Is dataset indicative of the training dataset used or the testing designs employed by the benchmarks? Page 2

“VERT” Page 2

The merely test their approach on OpenTitan, CVA6, Pulpissimo, OpenPiton. They didn’t say that this was a benchmark and of itself. Page 2

“20000” Page 2

They don’t test on 20000 designs. They test on like 16. Their benchmark is completely different. Page 2

“Limitation 3: Limited design scale and specification quality” Page 2

They have left out assertionbench here. But when we look at the plot we see that assertionbench is much much smaller than assertllm2, even though they both use free/opencores. For some reason assertionbench decided to just pick the first two categories and call it a day. they could have easily used the others too. But this is a noticeable improvement. Having 12 arithmetic cores isn’t really saying that much Page 2

“Most prior benchmarks [16, 17] focus on small module-level designs, rather than the larger and more complex IPlevel designs encountered in practice. The only benchmark targeting a larger-scale setting [18]" Page 2

FVEval and CVDP (Nvidia papers) have bite sized files. Both of these works target more than just assertion generation. That is why when we look at just assertion generation, we find that they are either too small or too few. Page 2

How AssertLLM2 alleviates the previously mentioned shortcomings Page 2

“❶ More complete and realistic task formulation." Page 2

“The first is bug-prevention. This scenario reflects the stage where RTL is still under development. Assertions are generated from the specification alone to capture intended behavior and help prevent design errors early. The second is bug-hunting. This scenario reflects the stage where RTL has been implemented but is not yet fully verified, and may therefore still contain functional bugs." Page 2

Need more sources about the typical workflow in FV Page 2

“Assertions are generated from the specification together with the RTL to test whether they can expose mismatches between intended behavior and implementation behavior." Page 2

“AssertLLM2 is the first benchmark to explicitly use buggy RTL as input to evaluate bug-detection capability." Page 2

“More rigorous evaluation” Page 2

“Beyond syntax and FPV, it evaluates COI coverage, proof coverage, formal coverage, and mutation-based bug detection." Page 2

“❸ Richer and more realistic designs and specifications” Page 2

“structured textual specification, the raw PDF, a verified golden RTL reference, and systematically mutated buggy RTL variants." Page 2

Each benchmark contains the above Page 2

“2 Problem Formulation” Page 3

I hate contrived formulas LLMs cannot be a function. A function by definition has to map to the same output every time when evaluated with some input. Page 3

“3 Benchmark Data Overview” Page 3

“AssertLLM2 comprises 83 real-world designs spanning 13 functional categories” Page 3

“AssertLLM2 also stands out from prior benchmarks in the scale of its designs." Page 3

“The buggy RTL variants include 20 single-bug variants and one five-bug variant obtained by combining five single-bug variants” Page 3

“realistic faulty design” Page 3

I don’t know if it is realistic. It is faulty. What do we mean by “realistic”? Are the faults indicative of common errors humans make? How did they find the common errors humans make? Page 3

“4 Benchmark Data Construction” Page 3

“4.1 Data Collection” Page 3

Collect designs from free/opencores, spinalHDL and RISC-mcu Page 3

“Finally, we require at least 200 lines of RTL code to filter out trivial designs." Page 3

“4.2 Structured Specification Construction” Page 3

Convert PDFs to plain text. They have a standardized template. Page 3

“This makes the documents difficult to use directly and creates a multimodal bottleneck for purely text-based open-source LLMs." Page 3

This is one of the points I have against spec+RTL. First of all we need spec which may not be always available. Second we need to convert that into a pure text format. What do we do about images? I know that LLMs can handle images and under the hood, there isn’t really a difference (the LLM only sees a token, doesn’t really care where it came from) but the sheer amount of text and the relations you can make with them nudge towards avoiding images. Page 3

“SPEC Tokens” Page 4

How are they measuring the number of tokens? tiktokenizer? Page 4

“Finally, human experts review the draft against the original documentation at the clause level. The resulting structured specification is therefore a curated and human-validated benchmark artifact." Page 4

Human in the loop Page 4

These are the mutations. They seem reasonable but I still feel icky about these being the bugs. What about logical errors? These are more like careless mistakes. I honestly don’t think a designer is missing an if branch. Maybe these are useful for a lint tool but the kinds of bugs we are looking for in formal are much deeper. I feel like all of these bugs can be revealed by just simulation. Formal bugs reveal a fundamental error in logic, in most cases. Page 5

![[assets/zimage-wuAssertLLM2ComprehensiveLLM2026-5-x70-y489.png]]

“4.3 Mutation-Based Buggy RTL Generation” Page 5

“5 Benchmark Evaluation Framework” Page 6

“6 Experimental Results” Page 7

“6.1 Experimental Setup” Page 7

“6.2 Overall Benchmark Results." Page 7

“6.3 Detailed Results on Selected Designs." Page 7

“7 Conclusion” Page 9

%% Import Date: 2026-07-01T15:44:14.047-04:00 %%